slope_comp — Mathlib

English

For a linear map f: E → F, slope (f ∘ g) a b = f(slope g a b).

Русский

Для линейного отображения f: E → F наклон композиции имеет вид slope (f ∘ g) a b = f(slope g a b).

LaTeX

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

Lean4

theorem slope_comp {F : Type*} [AddCommGroup F] [Module k F] (f : E →ₗ[k] F) (g : k → E) (a b : k) :
    slope (f ∘ g) a b = f (slope g a b) :=
  f.toAffineMap.slope_comp g a b

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