continuousAt_iff' — Mathlib

English

Convergence criterion for general nhds-nhds tendsto.

Русский

Критерий сходимости для общего случая сходимости через nhds.

LaTeX

$$Tendsto f (nhds a) (nhds b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ x, dist x a < δ → dist (f x) b < ε$$

Lean4

theorem continuousAt_iff' [TopologicalSpace β] {f : β → α} {b : β} :
    ContinuousAt f b ↔ ∀ ε > 0, ∀ᶠ x in 𝓝 b, dist (f x) (f b) < ε := by rw [ContinuousAt, tendsto_nhds]

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