union_sigma — Mathlib

English

For sets s1, s2 of indices and a family t, the sigma of their union distributes over union: (s1 ∪ s2).sigma t = s1.sigma t ∪ s2.sigma t.

Русский

Для множеств индексов s1, s2 и семейства t распределяется сигма-операция по объединению: (s1 ∪ s2).sigma t = s1.sigma t ∪ s2.sigma t.

LaTeX

$$union_sigma : (s1 ∪ s2).sigma t = s1.sigma t ∪ s2.sigma t$$

Lean4

@[simp]
theorem union_sigma : (s₁ ∪ s₂).sigma t = s₁.sigma t ∪ s₂.sigma t := by grind

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