of_comp — Mathlib

English

If the line derivative of the composite f ∘ L exists at x with value f' in direction v, then f has line derivative f' at Lx in direction Lv.

Русский

Если линейная производная композиции f ∘ L существует в точке x со значением f' по направлению v, то f имеет линейную производную f' в точке Lx по направлению Lv.

LaTeX

$$$$ HasLineDerivAt 𝕜 (f \circ L) f' x v \Rightarrow HasLineDerivAt 𝕜 f f' (L x) (L v) $$$$

Lean4

theorem of_comp {v : E'} (hf : HasLineDerivAt 𝕜 (f ∘ L) f' x v) : HasLineDerivAt 𝕜 f f' (L x) (L v) := by
  simpa [HasLineDerivAt] using hf

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