norm — Mathlib

English

If f is differentiable within s at x and f(x) ≠ 0, then y ↦ ‖f(y)‖ is differentiable within s at x.

Русский

Если f дифференцируема внутри s в x и f(x) ≠ 0, то y ↦ ‖f(y)‖ дифференцируема внутри s в x.

LaTeX

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

Lean4

theorem norm (hf : DifferentiableWithinAt ℝ f s x) (h0 : f x ≠ 0) : DifferentiableWithinAt ℝ (fun y => ‖f y‖) s x :=
  ((contDiffAt_id.norm 𝕜 h0).differentiableAt le_rfl).comp_differentiableWithinAt x hf

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