dist — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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