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.Modal.S4Point3McK.Kripke.instSoundLogicNatFormulaFrameClassS4Point3McKS4Point3McK : Sound Modal.S4Point3McK Kripke.FrameClass.S4Point3McK

instance LO.Modal.Modal.S4Point3McK.Kripke.instConsistentFormulaNatLogicS4Point3McK : Entailment.Consistent Modal.S4Point3McK

instance LO.Modal.Modal.S4Point3McK.Kripke.instCanonicalLogicNatS4Point3McKS4Point3McK : Kripke.Canonical Modal.S4Point3McK Kripke.FrameClass.S4Point3McK

instance LO.Modal.Modal.S4Point3McK.Kripke.instCompleteLogicNatFormulaFrameClassS4Point3McKS4Point3McK : Complete Modal.S4Point3McK Kripke.FrameClass.S4Point3McK

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

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