English
A copy construction for a generalized Heyting algebra preserving all the defining operations (le, top, sup, inf, himp, etc.).
Русский
Копирование обобщенной гейтинговой алгебры с сохранением всех основных операций
LaTeX
$$$\\exists c' : \\text{GeneralizedHeytingAlgebra }\\alpha\\;\\text{with preserved operations}$$$
Lean4
/-- A function to create a provable equal copy of a generalised heyting algebra
with possibly different definitional equalities. -/
def copy (c : GeneralizedHeytingAlgebra α) (le : α → α → Prop) (eq_le : le = (by infer_instance : LE α).le) (top : α)
(eq_top : top = (by infer_instance : Top α).top) (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) : GeneralizedHeytingAlgebra α
where
__ := Lattice.copy (@GeneralizedHeytingAlgebra.toLattice α c) le eq_le sup eq_sup inf eq_inf
__ := OrderTop.copy (@GeneralizedHeytingAlgebra.toOrderTop α c) top eq_top (by rw [← eq_le]; exact fun _ _ ↦ .rfl)
himp := himp
le_himp_iff _ _ _ := by simp [eq_le, eq_himp, eq_inf]
