English
Copy construction for a conditionally complete lattice preserving sSup, sInf and the conditional lattice structure.
Русский
Копирование условной полной решетки сохраняет sSup, sInf и условную структуру
LaTeX
$$$\\exists c' : \\text{ConditionallyCompleteLattice }\\alpha \\text{ with preserved data } le, sSup, sInf$$$
Lean4
/-- A function to create a provable equal copy of a conditionally complete lattice
with possibly different definitional equalities. -/
def copy (c : ConditionallyCompleteLattice α) (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) (sSup : Set α → α)
(eq_sSup : sSup = (by infer_instance : SupSet α).sSup) (sInf : Set α → α)
(eq_sInf : sInf = (by infer_instance : InfSet α).sInf) : ConditionallyCompleteLattice α
where
toLattice := Lattice.copy (@ConditionallyCompleteLattice.toLattice α c) le eq_le sup eq_sup inf eq_inf
sSup := sSup
sInf := sInf
le_csSup := by intro _ _ hb h; subst_vars; exact le_csSup _ _ hb h
csSup_le := by intro _ _ hb h; subst_vars; exact csSup_le _ _ hb h
csInf_le := by intro _ _ hb h; subst_vars; exact csInf_le _ _ hb h
le_csInf := by intro _ _ hb h; subst_vars; exact le_csInf _ _ hb h
