theorem
LO.System.disjunctive
{F : Type u_1}
{instβ : LO.LogicalConnective F}
{S : Type u_2}
{instβΒΉ : LO.System F S}
{π’ : S}
[self : LO.System.Disjunctive π’]
{Ο Ο : F}
:
Alias of LO.System.Disjunctive.disjunctive
.
theorem
LO.System.iff_disjunctive
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{π’ : S}
:
theorem
LO.System.iff_complete_disjunctive
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
[DecidableEq F]
{π’ : S}
[LO.System.Classical π’]
:
LO.System.Complete π’ β LO.System.Disjunctive π’