sUnion_iUnion — Mathlib

English

Let s_i be a family of subsets of Set α indexed by i ∈ I. Then the union of all unions ⋃₀ s_i equals the union over i of the union of s_i.

Русский

Пусть s_i — семейство множеств подмножеств α, тогда ⋃₀ ⋃ i, s_i = ⋃ i, ⋃₀ s_i.

LaTeX

$$$$ \bigcup_{\emptyset \neq A \in \bigcup_{i} s_i} A = \bigcup_{i} \bigcup_{A \in s_i} A $$$$

Lean4

theorem sUnion_iUnion (s : ι → Set (Set α)) : ⋃₀ ⋃ i, s i = ⋃ i, ⋃₀ s i := by
  simp only [sUnion_eq_biUnion, biUnion_iUnion]

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