mapL_comp — Mathlib

English

The functoriality of mapL with respect to composition: mapL (i ↦ g_i ∘ f_i) = mapL g ∘ mapL f.

Русский

Функториальность mapL по отношению к композиции: mapL (i ↦ g_i ∘ f_i) = mapL g ∘ mapL f.

LaTeX

$$$ \\mathrm{mapL}(\\lambda i, g_i \\circ f_i) = (\\mathrm{mapL}\\, g) \\circ (\\mathrm{mapL}\\, f) $$$

Lean4

theorem mapL_comp : mapL (fun (i : ι) ↦ g i ∘L f i) = mapL g ∘L mapL f :=
  by
  apply ContinuousLinearMap.coe_injective
  ext
  simp only [mapL_coe, ContinuousLinearMap.coe_comp, LinearMap.compMultilinearMap_apply, map_tprod, LinearMap.coe_comp,
    ContinuousLinearMap.coe_coe, Function.comp_apply]

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