def
LO.System.imply_BoxBoxdot_Box
{S : Type u_1}
{F : Type u_2}
[BasicModalLogicalConnective F]
[DecidableEq F]
[System F S]
{π’ : S}
[System.K4 π’]
{Ο : F}
:
Equations
Instances For
@[simp]
theorem
LO.System.imply_boxboxdot_box
{S : Type u_1}
{F : Type u_2}
[BasicModalLogicalConnective F]
[DecidableEq F]
[System F S]
{π’ : S}
[System.K4 π’]
{Ο : F}
:
def
LO.System.imply_Box_BoxBoxdot
{S : Type u_1}
{F : Type u_2}
[BasicModalLogicalConnective F]
[DecidableEq F]
[System F S]
{π’ : S}
[System.K4 π’]
{Ο : F}
:
Equations
Instances For
@[simp]
theorem
LO.System.imply_box_boxboxdot!
{S : Type u_1}
{F : Type u_2}
[BasicModalLogicalConnective F]
[DecidableEq F]
[System F S]
{π’ : S}
[System.K4 π’]
{Ο : F}
:
def
LO.System.imply_Box_BoxBoxdot'
{S : Type u_1}
{F : Type u_2}
[BasicModalLogicalConnective F]
[DecidableEq F]
[System F S]
{π’ : S}
[System.K4 π’]
{Ο : F}
(h : π’ β’ β‘Ο)
:
Instances For
def
LO.System.imply_Box_BoxBoxdot'!
{S : Type u_1}
{F : Type u_2}
[BasicModalLogicalConnective F]
[DecidableEq F]
[System F S]
{π’ : S}
[System.K4 π’]
{Ο : F}
(h : π’ β’! β‘Ο)
:
Equations
- β― = β―
Instances For
def
LO.System.iff_Box_BoxBoxdot
{S : Type u_1}
{F : Type u_2}
[BasicModalLogicalConnective F]
[DecidableEq F]
[System F S]
{π’ : S}
[System.K4 π’]
{Ο : F}
:
Equations
Instances For
@[simp]
theorem
LO.System.iff_box_boxboxdot!
{S : Type u_1}
{F : Type u_2}
[BasicModalLogicalConnective F]
[DecidableEq F]
[System F S]
{π’ : S}
[System.K4 π’]
{Ο : F}
:
def
LO.System.iff_Box_BoxdotBox
{S : Type u_1}
{F : Type u_2}
[BasicModalLogicalConnective F]
[DecidableEq F]
[System F S]
{π’ : S}
[System.K4 π’]
{Ο : F}
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LO.System.iff_box_boxdotbox!
{S : Type u_1}
{F : Type u_2}
[BasicModalLogicalConnective F]
[DecidableEq F]
[System F S]
{π’ : S}
[System.K4 π’]
{Ο : F}
:
def
LO.System.iff_Boxdot_BoxdotBoxdot
{S : Type u_1}
{F : Type u_2}
[BasicModalLogicalConnective F]
[DecidableEq F]
[System F S]
{π’ : S}
[System.K4 π’]
{Ο : F}
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LO.System.iff_boxdot_boxdotboxdot
{S : Type u_1}
{F : Type u_2}
[BasicModalLogicalConnective F]
[DecidableEq F]
[System F S]
{π’ : S}
[System.K4 π’]
{Ο : F}
:
def
LO.System.boxdotAxiomFour
{S : Type u_1}
{F : Type u_2}
[BasicModalLogicalConnective F]
[DecidableEq F]
[System F S]
{π’ : S}
[System.K4 π’]
{Ο : F}
:
Instances For
@[simp]
theorem
LO.System.boxdot_axiomFour!
{S : Type u_1}
{F : Type u_2}
[BasicModalLogicalConnective F]
[DecidableEq F]
[System F S]
{π’ : S}
[System.K4 π’]
{Ο : F}
: