sUnion_eq_biUnion — Mathlib

English

The union of a collection of sets equals the union over its elements indexed by S: ⋃₀ s = ⋃ (i ∈ S) i.

Русский

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

LaTeX

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

Lean4

theorem sUnion_eq_biUnion {s : Set (Set α)} : ⋃₀ s = ⋃ (i : Set α) (_ : i ∈ s), i := by rw [← sUnion_image, image_id']

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