hasFDerivAt_norm_smul_neg — Mathlib

English

If t < 0, then HasFDerivAt of the norm at t x holds for the negated linear functional; i.e., HasFDerivAt(‖·‖) (-f) (t • x) follows from HasFDerivAt(‖·‖) f x.

Русский

При t < 0 имеет место производная нормы для −f в точке t x, выводящаяся из производной f в x.

LaTeX

$$$t<0 \\Rightarrow HasFDerivAt(\\|\\cdot\\|) (-f) (t x) \\text{ from } HasFDerivAt(\\|\\cdot\\|) f x$$$

Lean4

theorem hasFDerivAt_norm_smul_neg (ht : t < 0) (h : HasFDerivAt (‖·‖) f x) : HasFDerivAt (‖·‖) (-f) (t • x) := by
  simpa [ht] using h.hasFDerivAt_norm_smul ht.ne

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