def
LO.System.iff_box_boxdot
{S : Type u_1}
{F : Type u_2}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
[LO.System F S]
{π’ : S}
[LO.System.S4 π’]
{Ο : F}
:
Equations
- LO.System.iff_box_boxdot = LO.System.iffIntro (LO.System.implyRightAnd LO.System.axiomT (LO.System.impId (β‘Ο))) LO.System.andβ
Instances For
@[simp]
theorem
LO.System.iff_box_boxdot!
{S : Type u_1}
{F : Type u_2}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
[LO.System F S]
{π’ : S}
[LO.System.S4 π’]
{Ο : F}
:
def
LO.System.iff_dia_diadot
{S : Type u_1}
{F : Type u_2}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
[LO.System F S]
{π’ : S}
[LO.System.S4 π’]
{Ο : F}
:
Equations
- LO.System.iff_dia_diadot = LO.System.iffIntro LO.System.orβ (LO.System.orβ'' LO.System.diaTc (LO.System.impId (βΟ)))
Instances For
@[simp]
theorem
LO.System.iff_dia_diadot!
{S : Type u_1}
{F : Type u_2}
[LO.BasicModalLogicalConnective F]
[DecidableEq F]
[LO.System F S]
{π’ : S}
[LO.System.S4 π’]
{Ο : F}
: