continuous_iff — Mathlib

English

A setwise version of continuity using nhdsWithin basis.

Русский

Версия непрерывности на множестве через nhdsWithin базис.

LaTeX

$$ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∀ᶠ x in 𝓝[s] b, dist (f x) (f b) < ε$$

Lean4

theorem continuous_iff [PseudoMetricSpace β] {f : α → β} :
    Continuous f ↔ ∀ b, ∀ ε > 0, ∃ δ > 0, ∀ a, dist a b < δ → dist (f a) (f b) < ε :=
  continuous_iff_continuousAt.trans <| forall_congr' fun _ => tendsto_nhds_nhds

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