English
Let for every index i a type G_i with a subset C_i ⊆ G_i and a type H_i with a subset D_i ⊆ H_i. Suppose we are given maps φ_i: G_i → H_i such that φ_i(C_i) ⊆ D_i on an 𝓕-large set of indices i (i.e., eventually). Then there is a canonical map between the restricted products, sending a family x = (x_i) with x_i ∈ C_i to the family (φ_i(x_i)) with φ_i(x_i) ∈ D_i for all large i.
Русский
Пусть для каждого индекса i задано множество G_i с подмножеством C_i и множество H_i с подмножеством D_i. Пусть даны отображения φ_i: G_i → H_i такие, что φ_i(C_i) ⊆ D_i для всех i из 𝓕-набора; тогда существует каноническое отображение между ограниченными произведениями, отправляющее семейство x_i∈C_i в семью φ_i(x_i)∈D_i (для больших i).
LaTeX
$$$\\operatorname{map} : \\prod^{\\mathrm{r}}_{i} (G_i, C_i)_{\\mathcal F} \\to \\prod^{\\mathrm{r}}_{i} (H_i, D_i)_{\\mathcal F}, \\quad (x_i)_i \\mapsto (\\varphi_i(x_i))_i,$ where $\\forall^{\\infty}_{i\\in\\mathcal F}\\, \\varphi_i(C_i) \\subseteq D_i$; i.e. $\\varphi_i(x_i) \\in D_i$ for i in a cofinal set.$$
Lean4
/-- The maps between restricted products over a fixed index type,
given maps on the factors. -/
def map {G H : ι → Type*} {C : (i : ι) → Set (G i)} {D : (i : ι) → Set (H i)} (φ : (i : ι) → G i → H i)
(hφ : ∀ᶠ i in 𝓕, MapsTo (φ i) (C i) (D i)) (x : Πʳ i, [G i, C i]_[𝓕]) : (Πʳ i, [H i, D i]_[𝓕]) :=
mapAlong G H id Filter.tendsto_id φ hφ x
