oscillationWithin_nhds_eq_oscillation

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]

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