norm — Mathlib

English

If f is ContDiff and never vanishes, then the map x ↦ ‖f(x)‖ is ContDiff.

Русский

Если f — континуально дифференцируемая и не обращающаяся к нулю, то x ↦ ‖f(x)‖ дифференцируема.

LaTeX

$$$$\text{ContDiff}_{\mathbb{R}}^n f \land \big(\forall x, f(x) \neq 0\big) \Rightarrow \text{ContDiff}_{\mathbb{R}}^n (x \mapsto \|f(x)\|).$$$$

Lean4

theorem norm (hf : ContDiffAt ℝ n f x) (h0 : f x ≠ 0) : ContDiffAt ℝ n (fun y => ‖f y‖) x :=
  (contDiffAt_norm 𝕜 h0).comp x hf

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