oscillation_eq_zero — Mathlib

English

If f is continuously within at D at x, then the oscillation of f within D at x is zero.

Русский

Если f непрерывна внутри D в x, то осцилляция внутри D в x равна нулю.

LaTeX

$$$\\text{ContinuousWithinAt}(f,D,x) \\Rightarrow \\operatorname{oscillationWithin}(f,D,x)=0$$$

Lean4

theorem oscillation_eq_zero [TopologicalSpace E] {f : E → F} {x : E} (hf : ContinuousAt f x) : oscillation f x = 0 :=
  by
  rw [← continuousWithinAt_univ f x] at hf
  exact oscillationWithin_univ_eq_oscillation f x ▸ hf.oscillationWithin_eq_zero

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