dist — Mathlib

English

If f and g are differentiable and f(x) ≠ g(x) for all x, then the map y ↦ dist(f(y), g(y)) is differentiable (as a real-valued function).

Русский

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

LaTeX

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

Lean4

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

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