English
Copy construction for a generalized co-Heyting algebra preserving all operations including sdiff.
Русский
Копирование обобщенной коейтинговой алгебры с сохранением операций, включая sdiff
LaTeX
$$$\\exists c' : \\text{GeneralizedCoheytingAlgebra }\\alpha\\;\\text{with preserved operations}$$$
Lean4
/-- A function to create a provable equal copy of a generalised co-Heyting algebra
with possibly different definitional equalities. -/
def copy (c : GeneralizedCoheytingAlgebra α) (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le) (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) : GeneralizedCoheytingAlgebra α
where
__ := Lattice.copy (@GeneralizedCoheytingAlgebra.toLattice α c) le eq_le sup eq_sup inf eq_inf
__ := OrderBot.copy (@GeneralizedCoheytingAlgebra.toOrderBot α c) bot eq_bot (by rw [← eq_le]; exact fun _ _ ↦ .rfl)
sdiff := sdiff
sdiff_le_iff := by simp [eq_le, eq_sdiff, eq_sup]
