class LO.Modal.Kripke.Frame.IsFiniteGrzPoint3 (F : Frame) extends F.IsFinite, F.IsPartialOrder, Std.Total F.Rel : Prop

• world_finite : Finite F.World
• refl (a : F.World) : F.Rel a a
• trans (a b c : F.World) : F.Rel a b → F.Rel b c → F.Rel a c
• antisymm (a b : F.World) : F.Rel a b → F.Rel b a → a = b
• total (a b : F.World) : F.Rel a b ∨ F.Rel b a

class LO.Modal.Kripke.Frame.IsFiniteGrzPoint3' (F : Frame) extends F.IsFinite, F.IsPartialOrder, IsPiecewiseStronglyConnected F.Rel : Prop

• world_finite : Finite F.World
• refl (a : F.World) : F.Rel a a
• trans (a b c : F.World) : F.Rel a b → F.Rel b c → F.Rel a c
• antisymm (a b : F.World) : F.Rel a b → F.Rel b a → a = b
• ps_connected : PiecewiseStronglyConnected F.Rel

@[reducible, inline]

abbrev LO.Modal.Kripke.FrameClass.finite_GrzPoint3 : FrameClass

Equations

• LO.Modal.Kripke.FrameClass.finite_GrzPoint3 = {F : LO.Modal.Kripke.Frame | F.IsFiniteGrzPoint3}

instance LO.Modal.Kripke.instIsFiniteGrzPoint2OfIsFiniteGrzPoint3 {F : Frame} [F.IsFiniteGrzPoint3] : F.IsFiniteGrzPoint2

instance LO.Modal.Kripke.instIsStronglyConnectedWhitepoint : whitepoint.IsStronglyConnected

instance LO.Modal.instSoundLogicNatFormulaFrameClassGrzPoint3Finite_GrzPoint3 : Sound Modal.GrzPoint3 Kripke.FrameClass.finite_GrzPoint3

instance LO.Modal.instSoundLogicNatFormulaSetFrameGrzPoint3SetOfIsFiniteGrzPoint3' : Sound Modal.GrzPoint3 {F : Kripke.Frame | F.IsFiniteGrzPoint3'}

instance LO.Modal.instConsistentFormulaNatLogicGrzPoint3 : Entailment.Consistent Modal.GrzPoint3

instance LO.Modal.instCompleteLogicNatFormulaFrameClassGrzPoint3Finite_GrzPoint3 : Complete Modal.GrzPoint3 Kripke.FrameClass.finite_GrzPoint3

instance LO.Modal.Logic.instStrictlyWeakerThanFormulaNatGrzPoint2GrzPoint3 : Modal.GrzPoint2 ⪱ Modal.GrzPoint3

instance LO.Modal.Logic.instStrictlyWeakerThanFormulaNatS4Point3GrzPoint3 : Modal.S4Point3 ⪱ Modal.GrzPoint3