class LO.Modal.Kripke.Frame.IsK45 (F : Frame) extends IsTrans F.World F.Rel, IsRightEuclidean F.Rel : Prop

• trans (a b c : F.World) : F.Rel a b → F.Rel b c → F.Rel a c
• reucl : RightEuclidean F.Rel

@[reducible, inline]

abbrev LO.Modal.Kripke.FrameClass.K45 : FrameClass

Equations

• LO.Modal.Kripke.FrameClass.K45 = {F : LO.Modal.Kripke.Frame | F.IsK45}

instance LO.Modal.Kripke.instIsK4Point3OfIsK45 {F : Frame} [F.IsK45] : F.IsK4Point3

instance LO.Modal.instSoundLogicNatFormulaFrameClassK45K45 : Sound Modal.K45 Kripke.FrameClass.K45

instance LO.Modal.instConsistentFormulaNatLogicK45 : Entailment.Consistent Modal.K45

instance LO.Modal.instCanonicalLogicNatK45K45 : Kripke.Canonical Modal.K45 Kripke.FrameClass.K45

instance LO.Modal.instCompleteLogicNatFormulaFrameClassK45K45 : Complete Modal.K45 Kripke.FrameClass.K45

instance LO.Modal.instStrictlyWeakerThanFormulaNatLogicK5K45 : Modal.K5 ⪱ Modal.K45

instance LO.Modal.instStrictlyWeakerThanFormulaNatLogicK4Point3K45 : Modal.K4Point3 ⪱ Modal.K45