continuousOn_iff'_left — Mathlib

English

ContinuousOn f s is equivalent to Tendsto (f x, f b) for all b ∈ s with nhdsWithin.

Русский

ContinuousOn f s эквивалентно Tendsto (f x, f b) для всех b ∈ s с nhdsWithin.

LaTeX

$$$\\text{ContinuousOn}(f,s) \\iff \\forall b \\in s, \\operatorname{Tendsto}(f x, f b) (\\mathcal{N}[s] b) (𝓤 α)$$$

Lean4

theorem continuousOn_iff'_left [TopologicalSpace β] {f : β → α} {s : Set β} :
    ContinuousOn f s ↔ ∀ b ∈ s, Tendsto (fun x => (f x, f b)) (𝓝[s] b) (𝓤 α) := by
  simp [ContinuousOn, continuousWithinAt_iff'_left]

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