lineDeriv_smul — Mathlib

English

For any c, lineDeriv 𝕜 f x (c • v) = c • lineDeriv 𝕜 f x v.

Русский

Для любого c: lineDeriv 𝕜 f x (c • v) = c • lineDeriv 𝕜 f x v.

LaTeX

$$$$ lineDeriv 𝕜 f x (c \cdot v) = c \cdot lineDeriv 𝕜 f x v $$$$

Lean4

theorem lineDeriv_smul {c : 𝕜} : lineDeriv 𝕜 f x (c • v) = c • lineDeriv 𝕜 f x v :=
  by
  rcases eq_or_ne c 0 with rfl | hc
  · simp [lineDeriv_zero]
  by_cases H : LineDifferentiableAt 𝕜 f x v
  · exact (H.hasLineDerivAt.smul c).lineDeriv
  · have H' : ¬(LineDifferentiableAt 𝕜 f x (c • v)) := by simpa [lineDifferentiableAt_smul_iff hc] using H
    simp [lineDeriv_zero_of_not_lineDifferentiableAt, H, H']

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