English
The value of mapAlong at j equals φ_j(x_{f(j)}).
Русский
Значение mapAlong в координате j равно φ_j(x_{f(j)}).
LaTeX
$$$ (\text{mapAlong}_{f}(x))_j = \phi_j(x_{f(j)}) $$$
Lean4
/-- Given two restricted products `Πʳ (i : ι₁), [R₁ i, A₁ i]_[𝓕₁]` and `Πʳ (j : ι₂), [R₂ j, A₂ j]_[𝓕₂]`,
`RestrictedProduct.mapAlong` gives a function between them. The data needed is a
function `f : ι₂ → ι₁` such that `𝓕₂` tends to `𝓕₁` along `f`, and functions `φ j : R₁ (f j) → R₂ j`
sending `A₁ (f j)` into `A₂ j` for an `𝓕₂`-large set of `j`'s.
See also `mapAlongMonoidHom`, `mapAlongAddMonoidHom` and `mapAlongRingHom` for variants.
-/
def mapAlong (x : Πʳ i, [R₁ i, A₁ i]_[𝓕₁]) : Πʳ j, [R₂ j, A₂ j]_[𝓕₂] :=
⟨fun j ↦ φ j (x (f j)), by filter_upwards [hf.eventually x.2, hφ] using fun _ h1 h2 ↦ h2 h1⟩
