linearMap_comp — Mathlib

English

The mapRange linear maps respect composition in two variables: mapRange.linearMap (f ∘ g) equals (mapRange.linearMap f) ∘ (mapRange.linearMap g).

Русский

MapRange линейные отображения сохраняют композицию: mapRange.linearMap (f ∘ g) = (mapRange.linearMap f) ∘ (mapRange.linearMap g).

LaTeX

$$$\\text{mapRange.linearMap}(f\\circ g) = (\\text{mapRange.linearMap} f) \\circ (\\text{mapRange.linearMap} g)$$$

Lean4

theorem linearMap_comp (f : N →ₛₗ[σ₂₃] P) (f₂ : M →ₛₗ[σ₁₂] N) :
    (mapRange.linearMap (f.comp f₂) : (α →₀ _) →ₛₗ[σ₁₃] _) = (mapRange.linearMap f).comp (mapRange.linearMap f₂) :=
  LinearMap.ext <| mapRange_comp f f.map_zero f₂ f₂.map_zero (comp f f₂).map_zero

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