mathlib documentation

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 bounded_lattice.copy {α : Type u} (c : bounded_lattice α) (le : α → α → Prop) (eq_le : le = bounded_lattice.le) (top : α) (eq_top : top = bounded_lattice.top) (bot : α) (eq_bot : bot = bounded_lattice.bot) (sup : α → α → α) (eq_sup : sup = bounded_lattice.sup) (inf : α → α → α) :

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

Equations
def distrib_lattice.copy {α : Type u} (c : distrib_lattice α) (le : α → α → Prop) (eq_le : le = distrib_lattice.le) (sup : α → α → α) (eq_sup : sup = distrib_lattice.sup) (inf : α → α → α) :

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

Equations
def complete_lattice.copy {α : Type u} (c : complete_lattice α) (le : α → α → Prop) (eq_le : le = complete_lattice.le) (top : α) (eq_top : top = complete_lattice.top) (bot : α) (eq_bot : bot = complete_lattice.bot) (sup : α → α → α) (eq_sup : sup = complete_lattice.sup) (inf : α → α → α) (eq_inf : inf = complete_lattice.inf) (Sup : set α → α) (eq_Sup : Sup = complete_lattice.Sup) (Inf : set α → α) :

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

Equations
def complete_distrib_lattice.copy {α : Type u} (c : complete_distrib_lattice α) (le : α → α → Prop) (eq_le : le = complete_distrib_lattice.le) (top : α) (eq_top : top = complete_distrib_lattice.top) (bot : α) (eq_bot : bot = complete_distrib_lattice.bot) (sup : α → α → α) (eq_sup : sup = complete_distrib_lattice.sup) (inf : α → α → α) (eq_inf : inf = complete_distrib_lattice.inf) (Sup : set α → α) (eq_Sup : Sup = complete_distrib_lattice.Sup) (Inf : set α → α) :

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

Equations
def conditionally_complete_lattice.copy {α : Type u} (c : conditionally_complete_lattice α) (le : α → α → Prop) (eq_le : le = conditionally_complete_lattice.le) (sup : α → α → α) (eq_sup : sup = conditionally_complete_lattice.sup) (inf : α → α → α) (eq_inf : inf = conditionally_complete_lattice.inf) (Sup : set α → α) (eq_Sup : Sup = conditionally_complete_lattice.Sup) (Inf : set α → α) :

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

Equations