continuousAt — Mathlib

English

If s is open, then ContinuousOn f s holds iff f is continuous at every point of s.

Русский

Если s открыто, то ContinuousOn f s эквивалентно непрерывности в каждой точке s.

LaTeX

$$$$\text{IsOpen}(s) \Rightarrow \Big(\text{ContinuousOn}(f,s) \iff \forall a\,(a\in s \to \text{ContinuousAt}(f,a))\Big).$$$$

Lean4

theorem continuousAt (h : ContinuousWithinAt f s x) (hs : s ∈ 𝓝 x) : ContinuousAt f x :=
  (continuousWithinAt_iff_continuousAt hs).mp h

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