tendsto_iff_edist_tendsto_0 — Mathlib

English

If f and g tend to a and b respectively, then edist(f, g) tends to edist(a,b).

Русский

Если функции сходятся, то расстояние между их значениями сходится к расстоянию между пределами.

LaTeX

$$$\text{Tendsto } f x (\mathcal{N} a) \land \text{Tendsto } g x (\mathcal{N} b) \Rightarrow \text{Tendsto } (\lambda x. edist (f x) (g x)) x (\mathcal{N}(edist a b)).$$$

Lean4

theorem tendsto_iff_edist_tendsto_0 {l : Filter β} {f : β → α} {y : α} :
    Tendsto f l (𝓝 y) ↔ Tendsto (fun x => edist (f x) y) l (𝓝 0) := by
  simp only [EMetric.nhds_basis_eball.tendsto_right_iff, EMetric.mem_ball, @tendsto_order ℝ≥0∞ β _ _,
    forall_prop_of_false ENNReal.not_lt_zero, forall_const, true_and]

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