English
A general construction copying a complete lattice with prescribed data for the order, top and bottom, and the sSup and sInf operations.
Русский
Обобщенная конструкция копирования полной решетки с заданными данными порядка, верхней и нижней границ и операций sup/inf над множествами
LaTeX
$$$\\exists c' : \\text{CompleteLattice }\\alpha \\;\\text{with data } le, top, bot, sup, inf, sSup, sInf$$$
Lean4
/-- A function to create a provable equal copy of a distributive lattice
with possibly different definitional equalities. -/
def copy (c : DistribLattice α) (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le) (sup : α → α → α)
(eq_sup : sup = (by infer_instance : Max α).max) (inf : α → α → α)
(eq_inf : inf = (by infer_instance : Min α).min) : DistribLattice α
where
toLattice := Lattice.copy (@DistribLattice.toLattice α c) le eq_le sup eq_sup inf eq_inf
le_sup_inf := by intros; simp [eq_le, eq_sup, eq_inf, le_sup_inf]
