range_piMap — Mathlib

English

For a family f_i : α_i → β_i, the range of the product map Pi.map f is the cartesian product of the ranges of the coordinate maps; i.e. range(Pi.map f) = pi univ i ↦ range(f_i).

Русский

Для семейства отображений f_i: α_i → β_i выполняется: range(Pi.map f) = ∏_i range(f_i).

LaTeX

$$$$ \\operatorname{range}(\\Pi f) = \\pi\\,\\mathrm{univ}\\,\\bigl(\\lambda i. \\mathrm{range}(f_i)\\bigr). $$$$

Lean4

@[simp]
theorem range_piMap (f : ∀ i, α i → β i) : range (Pi.map f) = pi univ fun i ↦ range (f i) := by
  simp only [← image_univ, ← piMap_image_univ_pi, pi_univ]

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