Documentation

Foundation.Modal.Kripke.Closure

@[reducible, inline]
Equations
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem LO.Modal.Kripke.Frame.RelReflTransGen.single {F : LO.Modal.Kripke.Frame} {x y : F.World} (hxy : x y) :
      x ≺^* y
      @[simp]
      theorem LO.Modal.Kripke.Frame.RelReflTransGen.reflexive {F : LO.Modal.Kripke.Frame} :
      Reflexive LO.Modal.Kripke.Frame.RelReflTransGen
      @[simp]
      theorem LO.Modal.Kripke.Frame.RelReflTransGen.transitive {F : LO.Modal.Kripke.Frame} :
      Transitive LO.Modal.Kripke.Frame.RelReflTransGen
      @[simp]
      theorem LO.Modal.Kripke.Frame.RelReflTransGen.symmetric {F : LO.Modal.Kripke.Frame} :
      Symmetric F.RelSymmetric LO.Modal.Kripke.Frame.RelReflTransGen
      @[reducible, inline]
      Equations
      Instances For
        @[reducible, inline]
        Equations
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem LO.Modal.Kripke.Frame.RelTransGen.single {F : LO.Modal.Kripke.Frame} {x y : F.World} (hxy : x y) :
            x ≺^+ y
            @[simp]
            theorem LO.Modal.Kripke.Frame.RelTransGen.transitive {F : LO.Modal.Kripke.Frame} :
            Transitive LO.Modal.Kripke.Frame.RelTransGen
            @[simp]
            theorem LO.Modal.Kripke.Frame.RelTransGen.symmetric {F : LO.Modal.Kripke.Frame} (hSymm : Symmetric F.Rel) :
            Symmetric LO.Modal.Kripke.Frame.RelTransGen
            @[reducible, inline]
            Equations
            Instances For
              theorem LO.Modal.Kripke.Frame.TransitiveClosure.single {F : LO.Modal.Kripke.Frame} {x y : F.World} (hxy : x y) :
              F^+.Rel x y
              @[reducible, inline]
              Equations
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[reducible, inline]
                  Equations
                  Instances For
                    @[reducible, inline]
                    Equations
                    Instances For
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[simp]
                        @[reducible, inline]
                        Equations
                        Instances For