English
For a finite index set ι, maps f_i: α_i → β_i and filters l_i on α_i, the same product-mapping identity holds without any surjectivity assumptions: map (Pi.map f) (pi l) = pi (i ↦ map (f_i) (l_i)).
Русский
Для конечного множества индексов ι, отображений f_i: α_i → β_i и фильтров l_i на α_i, верна та же тождество для произведений: map (Pi.map f) (pi l) = pi (i ↦ map (f_i) (l_i)).
LaTeX
$$$\\operatorname{map} (\\Pi.map f) (\\pi l) = \\pi (\\lambda i, \\operatorname{map} (f_i) (l_i))$$$
Lean4
/-- Given finite families of maps `f i : α i → β i` and of filters `l i : Filter (α i)`,
the indexed product of `f i`s maps the indexed product of the filters `l i`
to the indexed products of their pushforwards under individual `f i`s.
See also `map_piMap_pi` for a more general case.
-/
theorem map_piMap_pi_finite {α β : ι → Type*} [Finite ι] (f : ∀ i, α i → β i) (l : ∀ i, Filter (α i)) :
map (Pi.map f) (pi l) = pi fun i ↦ map (f i) (l i) :=
map_piMap_pi (by simp) l
