slope_comp — Mathlib

English

The slope of the composed map f ∘ g equals the linear part of f applied to the slope of g: slope (f ∘ g) a b = f.linear (slope g a b).

Русский

Уклон композиции f ∘ g равен линейной части отображения f, примененной к уклону g: slope (f ∘ g) a b = f.linear (slope g a b).

LaTeX

$$$\operatorname{slope}(f \circ g)\ a\ b = f.linear \bigl(\operatorname{slope}(g)\ a\ b\bigr)$$$

Lean4

theorem slope_comp {F PF : Type*} [AddCommGroup F] [Module k F] [AddTorsor F PF] (f : PE →ᵃ[k] PF) (g : k → PE)
    (a b : k) : slope (f ∘ g) a b = f.linear (slope g a b) := by
  simp only [slope, (· ∘ ·), f.linear.map_smul, f.linearMap_vsub]

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