dist — Mathlib

English

If f and g are ContDiffOn on s, and f x ≠ g x for all x ∈ s, then y ↦ dist(f(y), g(y)) is ContDiffOn on s.

Русский

Если f и g — ContDiffOn на s, и f(x) ≠ g(x) для всех x∈s, то y ↦ dist(f(y), g(y)) дифференцируема на s.

LaTeX

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

Lean4

theorem dist (hf : ContDiffOn ℝ n f s) (hg : ContDiffOn ℝ n g s) (hne : ∀ x ∈ s, f x ≠ g x) :
    ContDiffOn ℝ n (fun y => dist (f y) (g y)) s := fun x hx => (hf x hx).dist 𝕜 (hg x hx) (hne x hx)

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