prod_sup — Mathlib

English

Let s ∈ LowerSet α and t1, t2 ∈ LowerSet β. Then the product distributes over the join: s × (t1 ⊔ t2) = (s × t1) ⊔ (s × t2).

Русский

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

LaTeX

$$$ s \\times (t_1 \\sqcup t_2) = (s \\times t_1) \\sqcup (s \\times t_2) $$$

Lean4

@[simp]
theorem prod_sup : s ×ˢ (t₁ ⊔ t₂) = s ×ˢ t₁ ⊔ s ×ˢ t₂ :=
  ext prod_union

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