English
Let (f_i) be a family of linear maps f_i: β1_i → β2_i and (f2_i) a family of linear maps f2_i: β_i → β1_i. Then the global mapRange of the pointwise compositions equals the composition of the global mapRange maps: (mapRange.linearMap f) ∘ (mapRange.linearMap f2) = mapRange.linearMap (i ↦ f_i ∘ f2_i).
Русский
Пусть дана семья линейных отображений f_i: β1_i → β2_i и семья отображений f2_i: β_i → β1_i. Тогда глобальное отображение mapRange линейных отображений уважает композицию по точкам: (mapRange.linearMap f) ∘ (mapRange.linearMap f2) = mapRange.linearMap (i ↦ f_i ∘ f2_i).
LaTeX
$$$\\bigl(\\mathrm{mapRange.linearMap}\\; f\\bigr) \\circ \\bigl(\\mathrm{mapRange.linearMap}\\; f_2\\bigr) = \\mathrm{mapRange.linearMap}\\bigl(\\lambda i, (f_i) \\circ (f_{2,i})\\bigr)$$$
Lean4
theorem linearMap_comp (f : ∀ i, β₁ i →ₗ[R] β₂ i) (f₂ : ∀ i, β i →ₗ[R] β₁ i) :
(mapRange.linearMap fun i => (f i).comp (f₂ i)) = (mapRange.linearMap f).comp (mapRange.linearMap f₂) :=
LinearMap.ext <|
mapRange_comp (fun i x => f i x) (fun i x => f₂ i x) (fun i => (f i).map_zero) (fun i => (f₂ i).map_zero) (by simp)
