norm — Mathlib

English

If f,g are ContDiffWithinAt on a set s at x and f x ≠ g x for x ∈ s, then y ↦ dist(f(y), g(y)) is ContDiffWithinAt on s at x.

Русский

Если f и g — ContDiffWithinAt на множествах s в точке x и для x∈s выполняется f(x) ≠ g(x), то dist(f(y), g(y)) дифференцируема внутри s в x.

LaTeX

$$$$\text{ContDiffWithinAt}_{\mathbb{R}}^n f\,s\,x \land \text{ContDiffWithinAt}_{\mathbb{R}}^n g\,s\,x \land \forall x\in s\ f(x) \neq g(x) \Rightarrow \text{ContDiffWithinAt}_{\mathbb{R}}^n \big(y \mapsto \operatorname{dist}(f(y), g(y))\big)\,s\,x.$$$$

Lean4

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

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