sigma_union — Mathlib

English

Let s be a subset of ι, and for each i, let t1(i) and t2(i) be subsets of α(i). Then the sigma-construction over s of the union t1 ∪ t2 equals the union of the sigmas: s.sigma(t1) ∪ s.sigma(t2) = s.sigma(t1 ∪ t2).

Русский

Пусть s ⊆ ι и для каждого i даны множества t1(i), t2(i) ⊆ α(i). Тогда сигматическое объединение по s от t1(i) ∪ t2(i) равно объединению сигм: s.sigma(t1) ∪ s.sigma(t2) = s.sigma(t1 ∪ t2).

LaTeX

$$$s \sigma (i \mapsto t_1(i) \cup t_2(i)) = s \sigma t_1 \cup s \sigma t_2$$$

Lean4

@[simp]
theorem sigma_union : s.sigma (fun i ↦ t₁ i ∪ t₂ i) = s.sigma t₁ ∪ s.sigma t₂ := by grind

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