English
A copy operation that builds a distributive lattice from a given distributive lattice by reinterpreting all basic operations with possibly different definitional equalities.
Русский
Копирование распределенной решетки, сохраняющее распределенность при новой интерпретации операций
LaTeX
$$$\\exists c' : \\text{DistribLattice }\\alpha\\; (le' , top', bot', sup', inf', sSup', sInf') ,\\;\\text{le'...}$$$
Lean4
/-- A function to create a provable equal copy of a lattice
with possibly different definitional equalities. -/
def copy (c : Lattice α) (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) : Lattice α
where
le := le
sup := sup
inf := inf
lt := fun a b ↦ le a b ∧ ¬le b a
le_refl := by intros; simp [eq_le]
le_trans := by intro _ _ _ hab hbc; rw [eq_le] at hab hbc ⊢; exact le_trans hab hbc
le_antisymm := by intro _ _ hab hba; simp_rw [eq_le] at hab hba; exact le_antisymm hab hba
le_sup_left := by intros; simp [eq_le, eq_sup]
le_sup_right := by intros; simp [eq_le, eq_sup]
sup_le := by intro _ _ _ hac hbc; simp_rw [eq_le] at hac hbc ⊢; simp [eq_sup, hac, hbc]
inf_le_left := by intros; simp [eq_le, eq_inf]
inf_le_right := by intros; simp [eq_le, eq_inf]
le_inf := by intro _ _ _ hac hbc; simp_rw [eq_le] at hac hbc ⊢; simp [eq_inf, hac, hbc]
