instance LO.Modal.Neighborhood.instIsReflexiveSimple_blackhole : Frame.simple_blackhole.IsReflexive

class LO.Modal.Neighborhood.Frame.IsEMT (F : Frame) extends F.IsMonotonic, F.IsReflexive : Prop

• mono (X Y : Set F.World) : F.box (X ∩ Y) ⊆ F.box X ∩ F.box Y
• refl (X : Set F.World) : F.box X ⊆ X

@[reducible, inline]

abbrev LO.Modal.Neighborhood.FrameClass.EMT : FrameClass

Equations

• LO.Modal.Neighborhood.FrameClass.EMT = {F : LO.Modal.Neighborhood.Frame | F.IsEMT}

instance LO.Modal.instSoundLogicNatFormulaFrameClassEMTEMT : Sound Modal.EMT Neighborhood.FrameClass.EMT

instance LO.Modal.instConsistentFormulaNatLogicEMT : Entailment.Consistent Modal.EMT

instance LO.Modal.instCompleteLogicNatFormulaFrameClassEMTEMT : Complete Modal.EMT Neighborhood.FrameClass.EMT

instance LO.Modal.instStrictlyWeakerThanFormulaNatLogicEMEMT : Modal.EM ⪱ Modal.EMT