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_order.copy {α : Type u} {h h' : has_le α} (c : bounded_order α) (top : α) (eq_top : top = bounded_order.top) (bot : α) (eq_bot : bot = bounded_order.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
def lattice.copy {α : Type u} (c : lattice α) (le : α → α → Prop) (eq_le : le = lattice.le) (sup : α → α → α) (eq_sup : sup = lattice.sup) (inf : α → α → α) (eq_inf : inf = lattice.inf) :

A function to create a provable equal copy of a 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 : α → α → α) (eq_inf : inf = distrib_lattice.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 α → α) (eq_Inf : Inf = complete_lattice.Inf) :

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

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

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

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

A function to create a provable equal copy of a coframe 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 α → α) (eq_Inf : Inf = complete_distrib_lattice.Inf) :

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} (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 α → α) (eq_Inf : Inf = conditionally_complete_lattice.Inf) :

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

Equations