norm — Mathlib

English

If f is ContDiffOn and f(x) ≠ 0 for all x in its domain, then x ↦ ‖f(x)‖ is ContDiffOn.

Русский

Если f — ContDiffOn и для всех x в области определения f(x) ≠ 0, то x ↦ ‖f(x)‖ дифференцируема.

LaTeX

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

Lean4

theorem norm (hf : ContDiff ℝ n f) (h0 : ∀ x, f x ≠ 0) : ContDiff ℝ n fun y => ‖f y‖ :=
  contDiff_iff_contDiffAt.2 fun x => hf.contDiffAt.norm 𝕜 (h0 x)

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