@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Equations
- LO.Modal.Standard.Kripke.ReflexiveTransitiveConnectedFrameClass = {F : LO.Modal.Standard.Kripke.Frame | Reflexive F.Rel ∧ Transitive F.Rel ∧ Connected F.Rel}
Instances For
theorem
LO.Modal.Standard.Kripke.S4Dot3_defines
{α : Type u}
[Inhabited α]
[atleast : Atleast 2 α]
:
𝐒𝟒.𝟑.DefinesKripkeFrameClass LO.Modal.Standard.Kripke.ReflexiveTransitiveConnectedFrameClass
instance
LO.Modal.Standard.Kripke.instConsistentFormulaDeductionParameterS4Dot3
{α : Type u}
[Inhabited α]
[atleast : Atleast 2 α]
:
Equations
- ⋯ = ⋯
theorem
LO.Modal.Standard.Kripke.connected_CanonicalFrame
{α : Type u}
[DecidableEq α]
{Ax : LO.Modal.Standard.AxiomSet α}
(hAx : .𝟯 ⊆ Ax)
[LO.System.Consistent 𝝂Ax]
:
instance
LO.Modal.Standard.Kripke.instCompleteDeductionParameterFormulaDepS4Dot3AltReflexiveTransitiveConnectedFrameClass
{α : Type u}
[Inhabited α]
[DecidableEq α]
[atleast : Atleast 2 α]
:
Equations
- ⋯ = ⋯