Documentation

Foundation.Modal.Neighborhood.Logic.EC

source
@[reducible]
def LO.Modal.Neighborhood.Frame.IsEC (F : Frame) :
Prop

Alias of LO.Modal.Neighborhood.Frame.IsRegular.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Neighborhood.FrameClass.EC :
    FrameClass
    Equations
    Instances For
      source
      instance LO.Modal.EC.Neighborhood.sound :
      Sound Modal.EC Neighborhood.FrameClass.EC
      source
      instance LO.Modal.EC.consistent :
      Entailment.Consistent Modal.EC
      source
      instance LO.Modal.EC.Neighborhood.complete :
      Complete Modal.EC Neighborhood.FrameClass.EC
      source
      instance LO.Modal.instStrictlyWeakerThanFormulaNatLogicECECN :
      Modal.EC ⪱ Modal.ECN
      source
      instance LO.Modal.instStrictlyWeakerThanFormulaNatLogicECEMC :
      Modal.EC ⪱ Modal.EMC