mapAlong_apply — Mathlib

English

For restricted products, the j-th component of the mapped element is φ_j applied to the f(j)-component of the input.

Русский

Для ограниченного произведения j-ая компонента образа равна φ_j применению к компоненте f(j) входа.

LaTeX

$$$(x.mapAlong R_1 R_2 f hf φ hφ)(j) = φ_j\big(x(f(j))\big)$$$

Lean4

@[simp]
theorem mapAlong_apply (x : Πʳ i, [R₁ i, A₁ i]_[𝓕₁]) (j : ι₂) : x.mapAlong R₁ R₂ f hf φ hφ j = φ j (x (f j)) :=
  rfl

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