hasFDerivAt_norm_smul_pos — Mathlib

English

If t > 0, HasFDerivAt of the norm at t x equals HasFDerivAt of f at x; i.e., scaling by a positive t preserves the derivative in the same way as the nonzero case.

Русский

При t > 0 производная нормы в t x совпадает с производной в x.

LaTeX

$$$t>0 \\Rightarrow HasFDerivAt(\\|\\cdot\\|) f (t x) \\Leftrightarrow HasFDerivAt(\\|\\cdot\\|) f x$$$

Lean4

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

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