tendsto_iff_of_dist — Mathlib

English

If the distance between f1 and f2 tends to 0, then f1 and f2 have the same limit: Tendsto f1 p (nhds a) iff Tendsto f2 p (nhds a).

Русский

Если расстояние между f1 и f2 стремится к нулю, то f1 и f2 имеют один предел: сходимость f1 к a эквивалентна сходимости f2 к a.

LaTeX

$$$\operatorname{Tendsto}(f_1\, p)\,(\nhds a) \iff \operatorname{Tendsto}(f_2\, p)\,(\nhds a)$, при условии $\operatorname{Tendsto}(\lambda x. \operatorname{dist}(f_1 x)(f_2 x)) p (\nhds 0)$$$

Lean4

theorem tendsto_iff_of_dist {f₁ f₂ : ι → α} {p : Filter ι} {a : α} (h : Tendsto (fun x => dist (f₁ x) (f₂ x)) p (𝓝 0)) :
    Tendsto f₁ p (𝓝 a) ↔ Tendsto f₂ p (𝓝 a) :=
  Uniform.tendsto_congr <| tendsto_uniformity_iff_dist_tendsto_zero.2 h

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