continuousOn_iff' — Mathlib

English

Alternative formulation of Continuity on a set via nhdsWithin.

Русский

Альтернативная формулировка непрерывности на множестве через nhdsWithin.

LaTeX

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

Lean4

theorem continuousOn_iff' [TopologicalSpace β] {f : β → α} {s : Set β} :
    ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∀ᶠ x in 𝓝[s] b, dist (f x) (f b) < ε := by
  simp [ContinuousOn, continuousWithinAt_iff']

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