tendsto_congr — Mathlib

English

If (f,g) tends to the uniformity, then f and g have the same limit in nhds.

Русский

Если (f,g) пределы по равномерности, то f и g имеют общий предел в nhds.

LaTeX

$$$\\operatorname{Tendsto}(f,g) l (𝓤 β) \\Rightarrow (\\operatorname{Tendsto} f l (𝓝 b) \\iff \\operatorname{Tendsto} g l (𝓝 b))$$$

Lean4

theorem tendsto_congr {α β} [UniformSpace β] {f g : α → β} {l : Filter α} {b : β}
    (hfg : Tendsto (fun x => (f x, g x)) l (𝓤 β)) : Tendsto f l (𝓝 b) ↔ Tendsto g l (𝓝 b) :=
  ⟨fun h => h.congr_uniformity hfg, fun h => h.congr_uniformity hfg.uniformity_symm⟩

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