norm — Mathlib

English

If f is differentiable and never vanishes, then the map y ↦ ‖f(y)‖ is differentiable (as a real-valued function).

Русский

Если f дифференцируема и не принимает нулевые значения, то y ↦ ‖f(y)‖ дифференцируема по ℝ.

LaTeX

$$$\text{Differentiable}_{\mathbb{R}}(f) \land (\forall x, f(x) \neq 0) \Rightarrow \text{Differentiable}_{\mathbb{R}}(y \mapsto \|f(y)\|).$$$

Lean4

theorem norm (hf : Differentiable ℝ f) (h0 : ∀ x, f x ≠ 0) : Differentiable ℝ fun y => ‖f y‖ := fun x =>
  (hf x).norm 𝕜 (h0 x)

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