English
Copy for a complete lattice preserving sSup and sInf operations along with the lattice order.
Русский
Копирование полной решетки сохраняет операции над множествами-верхами и над множествами-низами
LaTeX
$$$\\exists c' : \\text{CompleteLattice }\\alpha \\text{ with } le, top, bot, sup, inf, sSup, sInf$$$
Lean4
/-- A function to create a provable equal copy of a complete lattice
with possibly different definitional equalities. -/
def copy (c : CompleteLattice α) (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) (sSup : Set α → α)
(eq_sSup : sSup = (by infer_instance : SupSet α).sSup) (sInf : Set α → α)
(eq_sInf : sInf = (by infer_instance : InfSet α).sInf) : CompleteLattice α
where
toLattice := Lattice.copy (@CompleteLattice.toLattice α c) le eq_le sup eq_sup inf eq_inf
top := top
bot := bot
sSup := sSup
sInf := sInf
le_sSup := by intro _ _ h; simp [eq_le, eq_sSup, le_sSup _ _ h]
sSup_le := by intro _ _ h; simpa [eq_le, eq_sSup] using h
sInf_le := by intro _ _ h; simp [eq_le, eq_sInf, sInf_le _ _ h]
le_sInf := by intro _ _ h; simpa [eq_le, eq_sInf] using h
le_top := by intros; simp [eq_le, eq_top]
bot_le := by intros; simp [eq_le, eq_bot]
