English
If D is a neighborhood of x, then the oscillation of f within D at x equals the oscillation of f at x.
Русский
Если D — окрестность x, то осциляция f внутри D в x равна осциляции f в x.
LaTeX
$$$\\text{If } D\\in\\mathcal{N}(x),\\; oscillationWithin(f,D,x) = oscillation(f,x).$$$
Lean4
/-- The oscillation of `f` at `x` within a neighborhood `D` of `x` is equal to `oscillation f x` -/
theorem oscillationWithin_nhds_eq_oscillation [TopologicalSpace E] (f : E → F) (D : Set E) (x : E) (hD : D ∈ 𝓝 x) :
oscillationWithin f D x = oscillation f x := by rw [oscillation, oscillationWithin, nhdsWithin_eq_nhds.2 hD]