continuousAt_iff — Mathlib

English

Equivalent local description of continuity via distance estimates.

Русский

Эквивалентное локальное описание непрерывности через расстояния.

LaTeX

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

Lean4

theorem continuousAt_iff [PseudoMetricSpace β] {f : α → β} {a : α} :
    ContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, dist x a < δ → dist (f x) (f a) < ε := by
  rw [ContinuousAt, tendsto_nhds_nhds]

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