class LO.Modal.Neighborhood.Frame.IsEMN (F : Frame) extends F.IsMonotonic, F.ContainsUnit : Prop

• mono (X Y : Set F.World) : F.box (X ∩ Y) ⊆ F.box X ∩ F.box Y
• contains_unit : F.box Set.univ = Set.univ

@[reducible, inline]

abbrev LO.Modal.Neighborhood.FrameClass.EMN : FrameClass

Equations

• LO.Modal.Neighborhood.FrameClass.EMN = {F : LO.Modal.Neighborhood.Frame | F.IsEMN}

instance LO.Modal.Neighborhood.instIsEMNCounterframe_axiomC₁ : counterframe_axiomC₁.IsEMN

instance LO.Modal.EMN.Neighborhood.sound : Sound Modal.EMN Neighborhood.FrameClass.EMN

instance LO.Modal.EMN.consistent : Entailment.Consistent Modal.EMN

instance LO.Modal.EMN.Neighborhood.complete : Complete Modal.EMN Neighborhood.FrameClass.EMN

instance LO.Modal.instStrictlyWeakerThanFormulaNatLogicEMNEMCN : Modal.EMN ⪱ Modal.EMCN