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.Hilbert.GLPoint3.Kripke.instSoundNormalNatFormulaFrameClassFinite_GLPoint3 : Sound Hilbert.GLPoint3 Kripke.FrameClass.finite_GLPoint3

instance LO.Modal.Hilbert.GLPoint3.Kripke.instConsistentFormulaNatNormal : Entailment.Consistent Hilbert.GLPoint3

instance LO.Modal.Hilbert.GLPoint3.Kripke.instCompleteNormalNatFormulaFrameClassFinite_GLPoint3 : Complete Hilbert.GLPoint3 Kripke.FrameClass.finite_GLPoint3

instance LO.Modal.Hilbert.GLPoint3.Kripke.instStrictlyWeakerThanFormulaNatNormalGL : Hilbert.GL ⪱ Hilbert.GLPoint3

instance LO.Modal.Hilbert.GLPoint3.Kripke.instStrictlyWeakerThanFormulaNatNormalK4Point3 : Hilbert.K4Point3 ⪱ Hilbert.GLPoint3

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

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