class LO.Modal.Kripke.Frame.IsFiniteGL (F : Frame) extends F.IsFinite, F.IsStrictPreorder : 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

@[reducible, inline]

abbrev LO.Modal.Kripke.FrameClass.finite_GL : FrameClass

Equations

• LO.Modal.Kripke.FrameClass.finite_GL = {F : LO.Modal.Kripke.Frame | F.IsFiniteGL}

instance LO.Modal.Kripke.instIsFiniteGLBlackpoint : blackpoint.IsFiniteGL

instance LO.Modal.Logic.GL.Kripke.instSoundNormalNatFormulaFrameClassGLFinite_GL : Sound Hilbert.GL Kripke.FrameClass.finite_GL

instance LO.Modal.Logic.GL.Kripke.instConsistentFormulaNatNormalGL : Entailment.Consistent Hilbert.GL

instance LO.Modal.instConsistentFormulaNatLogicGL : Entailment.Consistent Modal.GL