instHeytingAlgebra — Mathlib

English

If α and β are Heyting algebras, then their product α × β is a Heyting algebra, defined coordinatewise by (a,b) ⇨ (c,d) = (a ⇨ c, b ⇨ d).

Русский

Если α и β являются Хейтинговыми алгебрами, то их произведение α × β является Хейтинговой алгеброй, определяемой координатно: (a,b) ⇨ (c,d) = (a ⇨ c, b ⇨ d).

LaTeX

$$$\forall [\text{HeytingAlgebra }\alpha] [\text{HeytingAlgebra }\beta], \text{HeytingAlgebra}(\alpha \times \beta)$$$

Lean4

instance instHeytingAlgebra [HeytingAlgebra β] : HeytingAlgebra (α × β) where
  himp_bot a := Prod.ext_iff.2 ⟨himp_bot a.1, himp_bot a.2⟩

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