congr_dist — Mathlib

English

If f1 converges to a and the distance between f1 and f2 converges to 0, then f2 also converges to a.

Русский

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

LaTeX

$$$\text{Tendsto } f_1\, p\, (\nhd a) \land \text{Tendsto } (\lambda x. \operatorname{dist}(f_1 x)(f_2 x))\, p\, (\nhd 0) \Rightarrow \text{Tendsto } f_2\, p\, (\nhd a)$$$

Lean4

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

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