fderiv_norm_smul_neg — Mathlib

English

Let E be a real normed space. For any x ∈ E and t ∈ ℝ with t < 0, the derivative at t x equals the negative of the derivative at x; i.e., D‖·‖(t x) = −D‖·‖(x).

Русский

Пусть E - действительное нормированное пространство. Для любого x ∈ E и любого t ∈ ℝ с t < 0 производная нормы в точке t x равна минусу производной в точке x; то есть D‖·‖(t x) = −D‖·‖(x).

LaTeX

$$$t < 0 \\Rightarrow D(\\|\\cdot\\|)_{t x} = -\,D(\\|\\cdot\\|)_x$$$

Lean4

theorem fderiv_norm_smul_neg (ht : t < 0) : fderiv ℝ (‖·‖) (t • x) = -fderiv ℝ (‖·‖) x := by simp [fderiv_norm_smul, ht]

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