map_comp_ιMulti_family — Mathlib

English

For a family of vectors v: I → M, the map map n f on the image ιMulti_family R n v equals ιMulti_family R n (f∘v).

Русский

Для семейства векторов v: I → M отображение map n f на образе ιMulti_family R n v равно ιMulti_family R n (f∘v).

LaTeX

$$$ (map n f) \\circ (ιMulti\\_family R n v) = ιMulti\\_family R n (f \\circ v) $$$

Lean4

@[simp]
theorem map_comp_ιMulti_family {I : Type*} [LinearOrder I] (v : I → M) (f : M →ₗ[R] N) :
    (map n f) ∘ (ιMulti_family R n v) = ιMulti_family R n (f ∘ v) :=
  by
  ext ⟨s, hs⟩
  simp only [ιMulti_family, Function.comp_apply, map_apply_ιMulti]
  rfl

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