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) : BoundedOrder α

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

Equations

• BoundedOrder.copy c top eq_top bot eq_bot le_eq = BoundedOrder.mk

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) : Lattice α

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

Equations

• Lattice.copy c le eq_le sup eq_sup inf eq_inf = Lattice.mk (_ : ∀ (a b : α), inf a b ≤ a) (_ : ∀ (a b : α), inf a b ≤ b) (_ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c)

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) : DistribLattice α

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

Equations

• DistribLattice.copy c le eq_le sup eq_sup inf eq_inf = DistribLattice.mk (_ : ∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z)

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 = sSup) (sInf : Set α → α) (eq_sInf : sInf = sInf) : CompleteLattice α

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

Equations

• One or more equations did not get rendered due to their size.

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 = sSup) (sInf : Set α → α) (eq_sInf : sInf = sInf) : Order.Frame α

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

Equations

• One or more equations did not get rendered due to their size.

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 = sSup) (sInf : Set α → α) (eq_sInf : sInf = sInf) : Order.Coframe α

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

Equations

• One or more equations did not get rendered due to their size.

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 = sSup) (sInf : Set α → α) (eq_sInf : sInf = sInf) : CompleteDistribLattice α

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.

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 = sSup) (sInf : Set α → α) (eq_sInf : sInf = sInf) : ConditionallyCompleteLattice α

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

Equations

• One or more equations did not get rendered due to their size.