continuousOn_iff — Mathlib

English

Characterization of continuity on a set via pointwise ε-δ control within the set.

Русский

Характеризация непрерывности на множестве через ε-δ контроль внутри множества.

LaTeX

$$ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∃ δ > 0, ∀ a ∈ s, dist a b < δ → dist (f a) (f b) < ε$$

Lean4

theorem continuousOn_iff [PseudoMetricSpace β] {f : α → β} {s : Set α} :
    ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∃ δ > 0, ∀ a ∈ s, dist a b < δ → dist (f a) (f b) < ε := by
  simp [ContinuousOn, continuousWithinAt_iff]

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