Documentation

LeanPool.Incompleteness.Foundation.Modal.Kripke.SimpleExtension

SimpleExtension #

source
def LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension (F : FiniteTransitiveTree) :
FiniteTransitiveTree

Imported declaration from the Incompleteness formalization.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def LO.Modal.Kripke.«term_↧» :
    Lean.TrailingParserDescr

    Imported declaration from the Incompleteness formalization.

    Equations
    Instances For
      source
      @[implicit_reducible]
      instance LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.instCoeWorld {T : FiniteTransitiveTree} :
      Coe T.World T↧.World
      Equations
      source
      @[simp]
      theorem LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.root_not_original {T : FiniteTransitiveTree} {x : T.World} :
      Sum.inr x ≠ T↧.root
      source
      theorem LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.root_eq {T : FiniteTransitiveTree} :
      Sum.inl () = T↧.root
      source
      theorem LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.forth {T : FiniteTransitiveTree} {x y : T.World} (h : x ≺ y) :
      T↧.Rel (Sum.inr x) (Sum.inr y)
      source
      def LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.pMorphism {T : FiniteTransitiveTree} :
      T.toFrame →ₚ T↧.toFrame

      Imported declaration from the Incompleteness formalization.

      Equations
      Instances For
        source
        theorem LO.Modal.Kripke.FiniteTransitiveTree.SimpleExtension.through_original_root {T : FiniteTransitiveTree} {x : T↧.World} (h : T↧.root ≺ x) :
        x = Sum.inr T.root ∨ Sum.inr T.root ≺ x
        source
        @[reducible, inline]
        abbrev LO.Modal.Kripke.FiniteTransitiveTreeModel.SimpleExtension (M : FiniteTransitiveTreeModel) :
        FiniteTransitiveTreeModel

        Imported declaration from the Incompleteness formalization.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def LO.Modal.Kripke.«term_↧_1» :
          Lean.TrailingParserDescr

          Imported declaration from the Incompleteness formalization.

          Equations
          Instances For
            source
            @[implicit_reducible]
            instance LO.Modal.Kripke.FiniteTransitiveTreeModel.SimpleExtension.instCoeWorld {M : FiniteTransitiveTreeModel} :
            Coe M.World M↧.World
            Equations
            source
            def LO.Modal.Kripke.FiniteTransitiveTreeModel.SimpleExtension.pMorphism {M : FiniteTransitiveTreeModel} :
            M.toModel →ₚ M↧.toModel

            Imported declaration from the Incompleteness formalization.

            Equations
            Instances For
              source
              theorem LO.Modal.Kripke.FiniteTransitiveTreeModel.SimpleExtension.modal_equivalence_original_world {M : FiniteTransitiveTreeModel} {x : M.toModel.World} :
              x ↭ Sum.inr x