eq_zero_iff_continuousAt — Mathlib

English

The oscillation of f at x is zero if and only if f is continuous at x.

Русский

Осцилляция функции f в точке x равна нулю тогда и только тогда, когда f непрерывна в точке x.

LaTeX

$$$\\operatorname{oscillation}(f,x)=0 \\iff \\operatorname{ContinuousAt}(f,x)$$$

Lean4

/-- The oscillation of `f` at `x` is 0 if and only if `f` is continuous at `x`. -/
theorem eq_zero_iff_continuousAt [TopologicalSpace E] (f : E → F) (x : E) : oscillation f x = 0 ↔ ContinuousAt f x :=
  by
  rw [← oscillationWithin_univ_eq_oscillation, ← continuousWithinAt_univ f x]
  exact OscillationWithin.eq_zero_iff_continuousWithinAt f (mem_univ x)

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