sup_prod — Mathlib

English

Let s1, s2 be upper sets on α and t be an upper set on β. The product distributes over the supremum in the first factor: (s1 ⊔ s2) ×ˢ t = (s1 ×ˢ t) ⊔ (s2 ×ˢ t).

Русский

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

LaTeX

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

Lean4

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

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