iUnion_eq_range_sigma — Mathlib

English

For any f : Σ' i, s i → β, the union over i of s i equals the range of the PSigma-projected map: range f = ⋃ a, range (λ b, f ⟨a, b⟩).

Русский

Для любого f : Σ' i, s i → β объединение по i равно образу проекции PSigma: range f = ⋃ a, range (λ b, f ⟨a, b⟩).

LaTeX

$$$$ \\operatorname{range} f = \\bigcup_{a} \\operatorname{range} \\big( b \\mapsto f \\langle a, b \\rangle \\big). $$$$

Lean4

theorem iUnion_eq_range_sigma (s : α → Set β) : ⋃ i, s i = range fun a : Σ i, s i => a.2 := by simp [Set.ext_iff]

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