English
Construction that copies a Heyting algebra preserving all structural operations including implication.
Русский
Копирование гейтинговой алгебры с сохранением импликации и прочих операций
LaTeX
$$$\\exists c' : \\text{HeytingAlgebra }\\alpha \\text{ with preserved } le, top, bot, sup, inf, himp, compl$$$
Lean4
/-- A function to create a provable equal copy of a heyting algebra
with possibly different definitional equalities. -/
def copy (c : HeytingAlgebra α) (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) (himp : α → α → α)
(eq_himp : himp = (by infer_instance : HImp α).himp) (compl : α → α)
(eq_compl : compl = (by infer_instance : HasCompl α).compl) : HeytingAlgebra α
where
toGeneralizedHeytingAlgebra :=
GeneralizedHeytingAlgebra.copy (@HeytingAlgebra.toGeneralizedHeytingAlgebra α c) le eq_le top eq_top sup eq_sup inf
eq_inf himp eq_himp
__ := OrderBot.copy (@HeytingAlgebra.toOrderBot α c) bot eq_bot (by rw [← eq_le]; exact fun _ _ ↦ .rfl)
compl := compl
himp_bot := by simp [eq_le, eq_himp, eq_bot, eq_compl]
