Documentation

Foundation.Modal.Neighborhood.Logic.ED

source
instance LO.Modal.Neighborhood.instIsSerialSimple_blackhole :
Frame.simple_blackhole.IsSerial
source
@[reducible]
def LO.Modal.Neighborhood.Frame.IsED (F : Frame) :
Prop

Alias of LO.Modal.Neighborhood.Frame.IsSerial.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Neighborhood.FrameClass.ED :
    FrameClass
    Equations
    Instances For
      source
      instance LO.Modal.Neighborhood.instIsEDSimple_whitehole :
      Frame.simple_whitehole.IsED
      source
      instance LO.Modal.ED.Neighborhood.sound :
      Sound Modal.ED Neighborhood.FrameClass.ED
      source
      instance LO.Modal.ED.consistent :
      Entailment.Consistent Modal.ED
      source
      instance LO.Modal.instStrictlyWeakerThanFormulaNatLogicEDEND :
      Modal.ED ⪱ Modal.END