norm — Mathlib

English

If f is differentiable on s and f(x) ≠ 0 for all x ∈ s, then y ↦ ‖f(y)‖ is differentiable on s.

Русский

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

LaTeX

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

Lean4

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

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