prod_sup_prod — Mathlib

English

Let s1, s2 be upper sets in α and t1, t2 be upper sets in β. The product commutes with taking suprema in both arguments: s1 ×ˢ t1 ⊔ s2 ×ˢ t2 = (s1 ⊔ s2) ×ˢ (t1 ⊔ t2).

Русский

Пусть s1, s2 — верхние множества на α, а t1, t2 — верхние множества на β. Произведение сохраняет тождественную дистрибутивность по объединению в обеих аргументах: s1 ×ˢ t1 ⊔ s2 ×ˢ t2 = (s1 ⊔ s2) ×ˢ (t1 ⊔ t2).

LaTeX

$$$ s_1 \times^{\mathrm{S}} t_1 \sqcup s_2 \times^{\mathrm{S}} t_2 = (s_1 \sqcup s_2) \times^{\mathrm{S}} (t_1 \sqcup t_2) $$$

Lean4

theorem prod_sup_prod : s₁ ×ˢ t₁ ⊔ s₂ ×ˢ t₂ = (s₁ ⊔ s₂) ×ˢ (t₁ ⊔ t₂) :=
  ext prod_inter_prod

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