sUnion_eq_iUnion — Mathlib

English

The union of a collection of sets equals the union over the elements as a subtype: ⋃₀ s = ⋃ i : s, i.

Русский

Объединение множества подмножеств равно объединению элементов как подсета: ⋃₀ s = ⋃_{i ∈ s} i.

LaTeX

$$$$ \\bigcup S = \\bigcup_{i \\in S} i. $$$$

Lean4

theorem sUnion_eq_iUnion {s : Set (Set α)} : ⋃₀ s = ⋃ i : s, i := by simp only [← sUnion_range, Subtype.range_coe]

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