English
If α and β are generalized Heyting algebras, then α × β with coordinatewise order and implication is a generalized Heyting algebra.
Русский
Если α и β — обобщённые гейтинговы алгебры, то их произведение α × β с поперечным порядком и импликацией по координатам образуют обобщённую гейтингову алгебру.
LaTeX
$$$ [GeneralizedHeytingAlgebra \ α], [GeneralizedHeytingAlgebra \ β] \Rightarrow GeneralizedHeytingAlgebra (α \times β) \,\text{with } (x_1,y_1) \le (x_2,y_2) \Leftrightarrow x_1 \le x_2 \text{ и } y_1 \le y_2, \\ (x_1,y_1) \Rightarrow (x_2,y_2) = (x_1 \Rightarrow x_2, y_1 \Rightarrow y_2). $$$
Lean4
instance (priority := 100) toDistribLattice : DistribLattice α :=
DistribLattice.ofInfSupLe fun a b c => by simp_rw [inf_comm a, ← le_himp_iff, sup_le_iff, le_himp_iff, ← sup_le_iff];
rfl
