continuousWithinAt_iff'_left — Mathlib

English

For a subset s of β, ContinuousWithinAt f s b is equivalent to Tendsto (f x, f b) with the nhds within s.

Русский

Для подмножества s ⊆ β, ContinuousWithinAt f s b эквивалентно Tendsto (f x, f b) для nhdsWithin.

LaTeX

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

Lean4

theorem continuousWithinAt_iff'_left [TopologicalSpace β] {f : β → α} {b : β} {s : Set β} :
    ContinuousWithinAt f s b ↔ Tendsto (fun x => (f x, f b)) (𝓝[s] b) (𝓤 α) := by
  rw [ContinuousWithinAt, tendsto_nhds_left]

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