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.Hilbert.EMT.Neighborhood.instSoundWithRENatFormulaFrameClassEMT : Sound Hilbert.EMT Neighborhood.FrameClass.EMT

instance LO.Modal.Hilbert.EMT.Neighborhood.instConsistentFormulaNatWithRE : Entailment.Consistent Hilbert.EMT

instance LO.Modal.Hilbert.EMT.Neighborhood.instCompleteWithRENatFormulaFrameClassEMT : Complete Hilbert.EMT Neighborhood.FrameClass.EMT

instance LO.Modal.Hilbert.instStrictlyWeakerThanFormulaNatWithREEMEMT : Hilbert.EM ⪱ Hilbert.EMT

instance LO.Modal.instStrictlyWeakerThanFormulaNatLogicEMEMT : 𝐄𝐌 ⪱ 𝐄𝐌𝐓