Documentation

Mathlib.Order.Copy

Tooling to make copies of lattice structures #

Sometimes it is useful to make a copy of a lattice structure where one replaces the data parts with provably equal definitions that have better definitional properties.

def BoundedOrder.copy {α : Type u} {h : LE α} {h' : LE α} (c : BoundedOrder α) (top : α) (eq_top : top = ) (bot : α) (eq_bot : bot = ) (le_eq : ∀ (x y : α), x y x y) :

A function to create a provable equal copy of a bounded order with possibly different definitional equalities.

Equations
  • c.copy top eq_top bot eq_bot le_eq = BoundedOrder.mk
Instances For
    def Lattice.copy {α : Type u} (c : Lattice α) (le : ααProp) (eq_le : le = LE.le) (sup : ααα) (eq_sup : sup = Sup.sup) (inf : ααα) (eq_inf : inf = Inf.inf) :

    A function to create a provable equal copy of a lattice with possibly different definitional equalities.

    Equations
    • c.copy le eq_le sup eq_sup inf eq_inf = Lattice.mk
    Instances For
      def DistribLattice.copy {α : Type u} (c : DistribLattice α) (le : ααProp) (eq_le : le = LE.le) (sup : ααα) (eq_sup : sup = Sup.sup) (inf : ααα) (eq_inf : inf = Inf.inf) :

      A function to create a provable equal copy of a distributive lattice with possibly different definitional equalities.

      Equations
      Instances For
        def CompleteLattice.copy {α : Type u} (c : CompleteLattice α) (le : ααProp) (eq_le : le = LE.le) (top : α) (eq_top : top = ) (bot : α) (eq_bot : bot = ) (sup : ααα) (eq_sup : sup = Sup.sup) (inf : ααα) (eq_inf : inf = Inf.inf) (sSup : Set αα) (eq_sSup : sSup = SupSet.sSup) (sInf : Set αα) (eq_sInf : sInf = InfSet.sInf) :

        A function to create a provable equal copy of a complete lattice with possibly different definitional equalities.

        Equations
        • c.copy le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf sSup eq_sSup sInf eq_sInf = CompleteLattice.mk
        Instances For
          def Frame.copy {α : Type u} (c : Order.Frame α) (le : ααProp) (eq_le : le = LE.le) (top : α) (eq_top : top = ) (bot : α) (eq_bot : bot = ) (sup : ααα) (eq_sup : sup = Sup.sup) (inf : ααα) (eq_inf : inf = Inf.inf) (sSup : Set αα) (eq_sSup : sSup = SupSet.sSup) (sInf : Set αα) (eq_sInf : sInf = InfSet.sInf) :

          A function to create a provable equal copy of a frame with possibly different definitional equalities.

          Equations
          Instances For
            def Coframe.copy {α : Type u} (c : Order.Coframe α) (le : ααProp) (eq_le : le = LE.le) (top : α) (eq_top : top = ) (bot : α) (eq_bot : bot = ) (sup : ααα) (eq_sup : sup = Sup.sup) (inf : ααα) (eq_inf : inf = Inf.inf) (sSup : Set αα) (eq_sSup : sSup = SupSet.sSup) (sInf : Set αα) (eq_sInf : sInf = InfSet.sInf) :

            A function to create a provable equal copy of a coframe with possibly different definitional equalities.

            Equations
            Instances For
              def CompleteDistribLattice.copy {α : Type u} (c : CompleteDistribLattice α) (le : ααProp) (eq_le : le = LE.le) (top : α) (eq_top : top = ) (bot : α) (eq_bot : bot = ) (sup : ααα) (eq_sup : sup = Sup.sup) (inf : ααα) (eq_inf : inf = Inf.inf) (sSup : Set αα) (eq_sSup : sSup = SupSet.sSup) (sInf : Set αα) (eq_sInf : sInf = InfSet.sInf) :

              A function to create a provable equal copy of a complete distributive lattice with possibly different definitional equalities.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                def ConditionallyCompleteLattice.copy {α : Type u} (c : ConditionallyCompleteLattice α) (le : ααProp) (eq_le : le = LE.le) (sup : ααα) (eq_sup : sup = Sup.sup) (inf : ααα) (eq_inf : inf = Inf.inf) (sSup : Set αα) (eq_sSup : sSup = SupSet.sSup) (sInf : Set αα) (eq_sInf : sInf = InfSet.sInf) :

                A function to create a provable equal copy of a conditionally complete lattice with possibly different definitional equalities.

                Equations
                Instances For