norm — Mathlib

English

If f and g are differentiable at x and f(x) ≠ g(x), then the map y ↦ dist(f(y), g(y)) is differentiable at x.

Русский

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

LaTeX

$$$$\text{DifferentiableAt}_{\mathbb{R}} f x \land \text{DifferentiableAt}_{\mathbb{R}} g x \land f(x) \neq g(x) \Rightarrow \text{DifferentiableAt}_{\mathbb{R}} (\,y \mapsto \operatorname{dist}(f(y), g(y))\,) x.$$$$

Lean4

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

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