map_apply — Mathlib

English

For any x in the restricted product, the j-th component of its image under the map equals φ_j(x_j).

Русский

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

LaTeX

$$$\\big( \\operatorname{RestrictedProduct}.map(\\varphi, h_\\varphi\\, x) \\big)_j = \\varphi_j(x_j).$$$

Lean4

@[simp]
theorem map_apply {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]_[𝓕]) (j : ι) : x.map φ hφ j = φ j (x j) :=
  rfl

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