class LO.Modal.Kripke.Frame.IsS4Point3McK (F : Frame) extends IsRefl F.World F.Rel, IsTrans F.World F.Rel, IsPiecewiseConnected F.Rel, F.SatisfiesMcKinseyCondition : Prop

• 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
• p_connected : PiecewiseConnected F.Rel
• mckinsey (x : F.World) : ∃ (y : F.World), x ≺ y ∧ ∀ (z : F.World), y ≺ z → y = z

instance LO.Modal.Kripke.instIsS4Point2McKOfIsS4Point3McK {F : Frame} [F.IsS4Point3McK] : F.IsS4Point2McK

@[reducible, inline]

abbrev LO.Modal.Kripke.FrameClass.S4Point3McK : FrameClass

Equations

• LO.Modal.Kripke.FrameClass.S4Point3McK = {F : LO.Modal.Kripke.Frame | F.IsS4Point3McK}

instance LO.Modal.Hilbert.S4Point3McK.Kripke.instSoundNormalNatFormulaFrameClassS4Point3McK : Sound Hilbert.S4Point3McK Kripke.FrameClass.S4Point3McK

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

instance LO.Modal.Hilbert.S4Point3McK.Kripke.instCanonicalNormalNatS4Point3McK : Kripke.Canonical Hilbert.S4Point3McK Kripke.FrameClass.S4Point3McK

instance LO.Modal.Hilbert.S4Point3McK.Kripke.instCompleteNormalNatFormulaFrameClassS4Point3McK : Complete Hilbert.S4Point3McK Kripke.FrameClass.S4Point3McK

instance LO.Modal.Hilbert.S4Point3McK.Kripke.instStrictlyWeakerThanFormulaNatNormalS4Point2McK : Hilbert.S4Point2McK ⪱ Hilbert.S4Point3McK

instance LO.Modal.Hilbert.S4Point3McK.Kripke.instStrictlyWeakerThanFormulaNatNormalS4Point3 : Hilbert.S4Point3 ⪱ Hilbert.S4Point3McK

instance LO.Modal.instStrictlyWeakerThanFormulaNatLogicS4Point2McKS4Point3McK : Modal.S4Point2McK ⪱ Modal.S4Point3McK

instance LO.Modal.instStrictlyWeakerThanFormulaNatLogicS4Point3S4Point3McK : Modal.S4Point3 ⪱ Modal.S4Point3McK