English
Copy construction for a complete distributive lattice preserving all binary operations and distribution laws.
Русский
Копирование полной распределимой решетки сохраняет распределения
LaTeX
$$$\\exists c' : \\text{CompleteDistribLattice }\\alpha \\text{ with preserved } le, top, bot, sup, inf, sSup, sInf, sdiff, hnot, himp, compl$$$
Lean4
/-- A function to create a provable equal copy of a complete distributive lattice
with possibly different definitional equalities. -/
def copy (c : CompleteDistribLattice α) (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le) (top : α)
(eq_top : top = (by infer_instance : Top α).top) (bot : α) (eq_bot : bot = (by infer_instance : Bot α).bot)
(sup : α → α → α) (eq_sup : sup = (by infer_instance : Max α).max) (inf : α → α → α)
(eq_inf : inf = (by infer_instance : Min α).min) (sdiff : α → α → α)
(eq_sdiff : sdiff = (by infer_instance : SDiff α).sdiff) (hnot : α → α)
(eq_hnot : hnot = (by infer_instance : HNot α).hnot) (himp : α → α → α)
(eq_himp : himp = (by infer_instance : HImp α).himp) (compl : α → α)
(eq_compl : compl = (by infer_instance : HasCompl α).compl) (sSup : Set α → α)
(eq_sSup : sSup = (by infer_instance : SupSet α).sSup) (sInf : Set α → α)
(eq_sInf : sInf = (by infer_instance : InfSet α).sInf) : CompleteDistribLattice α
where
toFrame :=
Frame.copy (@CompleteDistribLattice.toFrame α c) le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf himp eq_himp
compl eq_compl sSup eq_sSup sInf eq_sInf
__ :=
Coframe.copy (@CompleteDistribLattice.toCoframe α c) le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf sdiff
eq_sdiff hnot eq_hnot sSup eq_sSup sInf eq_sInf
