English
Let f_i : α_i → β_i be a family of maps and t_i ⊆ α_i. Then the image of Pi.map f on the universal product univ.pi t equals the universal product of the coordinatewise images, i.e. the full product of f_i''t_i.
Русский
Пусть f_i : α_i → β_i, и для каждого i множество t_i ⊆ α_i. Тогда образ Pi.map f над полным произведением univ.pi t равен полному произведению образов по координатам: image(Pi.map f)(univ.pi t) = univ.pi (i ↦ f_i''t_i).
LaTeX
$$$$ \\operatorname{image}(\\Pi f)(\\mathrm{univ} \\pi t) = \\mathrm{univ} \\pi \\bigl(i \\mapsto f_i'' t_i\\bigr). $$$$
Lean4
theorem piMap_image_univ_pi (f : ∀ i, α i → β i) (t : ∀ i, Set (α i)) :
Pi.map f '' univ.pi t = univ.pi fun i ↦ f i '' t i :=
piMap_image_pi (by simp) t
