range_sigma_eq_iUnion_range — Mathlib

English

For any f : Σ γ → β with γ : α → Type*, the union over i of s i equals the range of f restricted to the second coordinate: range f = ⋃ a, range (f ⟨a, ·⟩).

Русский

Для любого f : Σ γ → β, где γ : α → Type*, объединение по i равняется образу функции f по второй координате: range f = ⋃ a, range (f ⟨a, ·⟩).

LaTeX

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

Lean4

theorem range_sigma_eq_iUnion_range {γ : α → Type*} (f : Sigma γ → β) : range f = ⋃ a, range fun b => f ⟨a, b⟩ :=
  Set.ext <| by simp

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