continuousOn_iff'_right — Mathlib

English

ContinuousOn f s is equivalent to pointwise tendsto to the uniformity for each b ∈ s.

Русский

ContinuousOn f s эквивалентно тождению в точках: для каждого b ∈ s Tendsto к 𝓤 α.

LaTeX

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

Lean4

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

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