prod_sup — Mathlib

English

Let s be an upper set in α and t1, t2 be upper sets in β. The product distributes over the supremum in the second factor: s ×ˢ (t1 ⊔ t2) = s ×ˢ t1 ⊔ s ×ˢ t2.

Русский

Пусть s — верхнее множество в α, а t1, t2 — верхние множества в β. Произведение распределяется по суми во второй компоненте: s ×ˢ (t1 ⊔ t2) = s ×ˢ t1 ⊔ s ×ˢ t2.

LaTeX

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

Lean4

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

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