Documentation

Foundation.Modal.Neighborhood.Logic.ET

source
instance LO.Modal.Neighborhood.instIsReflexiveSimple_blackhole :
Frame.simple_blackhole.IsReflexive
source
@[reducible]
def LO.Modal.Neighborhood.Frame.IsET (F : Frame) :
Prop

Alias of LO.Modal.Neighborhood.Frame.IsReflexive.

Equations
Instances For
    source
    class LO.Modal.Neighborhood.Frame.IsFiniteET (F : Frame) extends F.IsReflexive, F.IsFinite :
    Prop
    Instances
      source
      @[reducible, inline]
      abbrev LO.Modal.Neighborhood.FrameClass.ET :
      FrameClass
      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev LO.Modal.Neighborhood.FrameClass.finite_ET :
        FrameClass
        Equations
        Instances For
          source
          instance LO.Modal.Neighborhood.instIsSerialOfIsReflexive {F : Frame} [F.IsReflexive] :
          F.IsSerial
          source
          instance LO.Modal.ET.Neighborhood.sound :
          Sound Modal.ET Neighborhood.FrameClass.ET
          source
          instance LO.Modal.ET.consistent :
          Entailment.Consistent Modal.ET
          source
          instance LO.Modal.ET.Neighborhood.complete :
          Complete Modal.ET Neighborhood.FrameClass.ET
          source
          instance LO.Modal.instStrictlyWeakerThanFormulaNatLogicEDET :
          Modal.ED ⪱ Modal.ET