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 OrderTop.copy {α : Type u} {h h' : LE α} (c : OrderTop α) (top : α) (eq_top : top = ) (le_eq : ∀ (x y : α), x y x y) :

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

Equations
    Instances For
      def OrderBot.copy {α : Type u} {h h' : LE α} (c : OrderBot α) (bot : α) (eq_bot : bot = ) (le_eq : ∀ (x y : α), x y x y) :

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

      Equations
        Instances For
          def BoundedOrder.copy {α : Type u} {h 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
            Instances For
              def Lattice.copy {α : Type u} (c : Lattice α) (le : ααProp) (eq_le : le = LE.le) (sup : ααα) (eq_sup : sup = max) (inf : ααα) (eq_inf : inf = min) :

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

              Equations
                Instances For
                  def DistribLattice.copy {α : Type u} (c : DistribLattice α) (le : ααProp) (eq_le : le = LE.le) (sup : ααα) (eq_sup : sup = max) (inf : ααα) (eq_inf : inf = min) :

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

                  Equations
                    Instances For
                      def GeneralizedHeytingAlgebra.copy {α : Type u} (c : GeneralizedHeytingAlgebra α) (le : ααProp) (eq_le : le = LE.le) (top : α) (eq_top : top = ) (sup : ααα) (eq_sup : sup = max) (inf : ααα) (eq_inf : inf = min) (himp : ααα) (eq_himp : himp = HImp.himp) :

                      A function to create a provable equal copy of a generalised heyting algebra with possibly different definitional equalities.

                      Equations
                        Instances For
                          def GeneralizedCoheytingAlgebra.copy {α : Type u} (c : GeneralizedCoheytingAlgebra α) (le : ααProp) (eq_le : le = LE.le) (bot : α) (eq_bot : bot = ) (sup : ααα) (eq_sup : sup = max) (inf : ααα) (eq_inf : inf = min) (sdiff : ααα) (eq_sdiff : sdiff = SDiff.sdiff) :

                          A function to create a provable equal copy of a generalised coheyting algebra with possibly different definitional equalities.

                          Equations
                            Instances For
                              def HeytingAlgebra.copy {α : Type u} (c : HeytingAlgebra α) (le : ααProp) (eq_le : le = LE.le) (top : α) (eq_top : top = ) (bot : α) (eq_bot : bot = ) (sup : ααα) (eq_sup : sup = max) (inf : ααα) (eq_inf : inf = min) (himp : ααα) (eq_himp : himp = HImp.himp) (compl : αα) (eq_compl : compl = HasCompl.compl) :

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

                              Equations
                                Instances For
                                  def CoheytingAlgebra.copy {α : Type u} (c : CoheytingAlgebra α) (le : ααProp) (eq_le : le = LE.le) (top : α) (eq_top : top = ) (bot : α) (eq_bot : bot = ) (sup : ααα) (eq_sup : sup = max) (inf : ααα) (eq_inf : inf = min) (sdiff : ααα) (eq_sdiff : sdiff = SDiff.sdiff) (hnot : αα) (eq_hnot : hnot = HNot.hnot) :

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

                                  Equations
                                    Instances For
                                      def BiheytingAlgebra.copy {α : Type u} (c : BiheytingAlgebra α) (le : ααProp) (eq_le : le = LE.le) (top : α) (eq_top : top = ) (bot : α) (eq_bot : bot = ) (sup : ααα) (eq_sup : sup = max) (inf : ααα) (eq_inf : inf = min) (sdiff : ααα) (eq_sdiff : sdiff = SDiff.sdiff) (hnot : αα) (eq_hnot : hnot = HNot.hnot) (himp : ααα) (eq_himp : himp = HImp.himp) (compl : αα) (eq_compl : compl = HasCompl.compl) :

                                      A function to create a provable equal copy of a biheyting algebra 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 = max) (inf : ααα) (eq_inf : inf = min) (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
                                            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 = max) (inf : ααα) (eq_inf : inf = min) (himp : ααα) (eq_himp : himp = HImp.himp) (compl : αα) (eq_compl : compl = HasCompl.compl) (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 = max) (inf : ααα) (eq_inf : inf = min) (sdiff : ααα) (eq_sdiff : sdiff = SDiff.sdiff) (hnot : αα) (eq_hnot : hnot = HNot.hnot) (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 = max) (inf : ααα) (eq_inf : inf = min) (sdiff : ααα) (eq_sdiff : sdiff = SDiff.sdiff) (hnot : αα) (eq_hnot : hnot = HNot.hnot) (himp : ααα) (eq_himp : himp = HImp.himp) (compl : αα) (eq_compl : compl = HasCompl.compl) (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
                                                        Instances For
                                                          def ConditionallyCompleteLattice.copy {α : Type u} (c : ConditionallyCompleteLattice α) (le : ααProp) (eq_le : le = LE.le) (sup : ααα) (eq_sup : sup = max) (inf : ααα) (eq_inf : inf = min) (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