class LO.Modal.Neighborhood.Frame.IsEMT4 (F : Frame) extends F.IsMonotonic, F.IsReflexive, F.IsTransitive : 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
• trans (X : Set F.World) : F.box X ⊆ F.box^[2] X

@[reducible, inline]

abbrev LO.Modal.Neighborhood.FrameClass.EMT4 : FrameClass

Equations

• LO.Modal.Neighborhood.FrameClass.EMT4 = {F : LO.Modal.Neighborhood.Frame | F.IsEMT4}

class LO.Modal.Neighborhood.Frame.IsFiniteEMT4 (F : Frame) extends F.IsEMT4, F.IsFinite : 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
• trans (X : Set F.World) : F.box X ⊆ F.box^[2] X
• world_finite : Finite F.World

@[reducible, inline]

abbrev LO.Modal.Neighborhood.FrameClass.finite_EMT4 : FrameClass

Equations

• LO.Modal.Neighborhood.FrameClass.finite_EMT4 = {F : LO.Modal.Neighborhood.Frame | F.IsFiniteEMT4}

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

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

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

instance LO.Modal.EMT4.Neighborhood.finite_complete : Complete Modal.EMT4 Neighborhood.FrameClass.finite_EMT4

FFP of Modal.EMT4