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)