sup_prod — Mathlib

English

Let s1, s2 be lower sets in α and t be a lower set in β. 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 union_prod

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