continuousWithinAt_univ — Mathlib

English

If f is continuous within s at x, then f tends to f x along nhdsWithin x s and within nhdsWithin (f x) (image f s).

Русский

Если f непрерывна внутри s в точке x, то она стремится к f(x) вдоль nhdsWithin x s и вдоль nhdsWithin (f(x)) (образ f в s).

LaTeX

$$$ (h : ContinuousWithinAt f s x) \\Rightarrow Tendsto f (\\mathcal{N} [s] x) (\\mathcal{N}[(image f s)] (f x)) $$$

Lean4

theorem continuousWithinAt_univ (f : α → β) (x : α) : ContinuousWithinAt f Set.univ x ↔ ContinuousAt f x := by
  rw [ContinuousAt, ContinuousWithinAt, nhdsWithin_univ]

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