instGeneralizedHeytingAlgebra — Mathlib

English

If α and β are generalized Heyting algebras, then their Cartesian product α × β carries a natural generalized Heyting algebra structure componentwise.

Русский

Если α и β являются обобщёнными гейтинговыми алгебрами, то их декартово произведение α × β естественным образом обладает структурой обобщённой гейтинговой алгебры по компонентам.

LaTeX

$$$\text{GeneralizedHeytingAlgebra}(\alpha) \land \text{GeneralizedHeytingAlgebra}(\beta) \Rightarrow \text{GeneralizedHeytingAlgebra}(\alpha \times \beta)$$$

Lean4

instance instGeneralizedHeytingAlgebra [GeneralizedHeytingAlgebra β] : GeneralizedHeytingAlgebra (α × β) where
  le_himp_iff _ _ _ := and_congr le_himp_iff le_himp_iff

Похожие утверждения