continuousAt_iff'_right — Mathlib

English

A function f: β → α is continuous at b if and only if its paired map (f b, f x) tends to the diagonal uniformity as x→b.

Русский

Функция f: β → α непрерывна в точке b тогда и только тогда, когда отображение x ↦ (f b, f x) стремится к диагональной равномерности при x→b.

LaTeX

$$$\\text{ContinuousAt}(f,b) \\iff \\operatorname{Tendsto}(\\lambda x. (f b, f x)) (\\mathcal{N}(b)) (\\mathcal{U}(α))$$$

Lean4

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

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