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