theorem Finite.of_scoped_subtype {α : Sort u_1} {P Q : α → Prop} (h : ∀ (x : α), Q x → P x) [Finite { x : α // P x }] : Finite { x : α // Q x }

class LO.Modal.Kripke.Frame.IsFiniteGLPoint3 (F : Frame) extends F.IsFiniteGL, IsTrichotomous F.World F.Rel : Prop

• world_finite : Finite F.World
• irrefl (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
• trichotomous (a b : F.World) : F.Rel a b ∨ a = b ∨ F.Rel b a

class LO.Modal.Kripke.Frame.IsFiniteGLPoint3' (F : Frame) extends F.IsFiniteGL, IsPiecewiseConnected F.Rel : Prop

• world_finite : Finite F.World
• irrefl (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
• p_connected : PiecewiseConnected F.Rel

@[reducible, inline]

abbrev LO.Modal.Kripke.FrameClass.finite_GLPoint3 : FrameClass

Equations

• LO.Modal.Kripke.FrameClass.finite_GLPoint3 = {F : LO.Modal.Kripke.Frame | F.IsFiniteGLPoint3}

instance LO.Modal.Kripke.instIsFiniteGLPoint3Blackpoint : blackpoint.IsFiniteGLPoint3

instance LO.Modal.Modal.GLPoint3.Kripke.instSoundLogicNatFormulaFrameClassGLPoint3Finite_GLPoint3 : Sound Modal.GLPoint3 Kripke.FrameClass.finite_GLPoint3

instance LO.Modal.Modal.GLPoint3.Kripke.instSoundLogicNatFormulaSetFrameGLPoint3SetOfIsFiniteGLPoint3' : Sound Modal.GLPoint3 {F : Kripke.Frame | F.IsFiniteGLPoint3'}

instance LO.Modal.Modal.GLPoint3.Kripke.instConsistentFormulaNatLogicGLPoint3 : Entailment.Consistent Modal.GLPoint3

instance LO.Modal.Modal.GLPoint3.Kripke.instWeakerThanFormulaNatLogicKGLPoint3 : Modal.K ⪯ Modal.GLPoint3

instance LO.Modal.Modal.GLPoint3.Kripke.complete : Complete Modal.GLPoint3 Kripke.FrameClass.finite_GLPoint3

instance LO.Modal.Modal.GLPoint3.Kripke.instStrictlyWeakerThanFormulaNatLogicGLGLPoint3 : Modal.GL ⪱ Modal.GLPoint3

instance LO.Modal.Modal.GLPoint3.Kripke.instStrictlyWeakerThanFormulaNatLogicK4Point3GLPoint3 : Modal.K4Point3 ⪱ Modal.GLPoint3