instCoheytingAlgebra — Mathlib

English

The Cartesian product of two co-Heyting algebras is again a co-Heyting algebra, defined componentwise.

Русский

Декартово произведение двух коейтиинговых алгебр также является коейтинговой алгеброй, определяемой покомпонентно.

LaTeX

$$$\text{sdiff}_{\alpha\times\beta}((a_1,a_2),(b_1,b_2)) = (a_1 \setminus b_1, a_2 \setminus b_2) \quad\text{and}\quad \text{top\_sdiff}((a_1,a_2)) = (\top\!_\alpha, \top\!_\beta).$$$

Lean4

instance instCoheytingAlgebra [CoheytingAlgebra β] : CoheytingAlgebra (α × β)
    where
  sdiff_le_iff _ _ _ := and_congr sdiff_le_iff sdiff_le_iff
  top_sdiff a := Prod.ext_iff.2 ⟨top_sdiff' a.1, top_sdiff' a.2⟩

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