continuousAt_iff'_left — Mathlib

English

If the pair (f,g) converges to the uniformity, then f and g have the same limit.

Русский

Если пара функций (f,g) сходится к равномерности, то f и g имеют одинаковый предел.

LaTeX

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

Lean4

theorem continuousAt_iff'_left [TopologicalSpace β] {f : β → α} {b : β} :
    ContinuousAt f b ↔ Tendsto (fun x => (f x, f b)) (𝓝 b) (𝓤 α) := by rw [ContinuousAt, tendsto_nhds_left]

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