oscillationWithin_univ_eq_oscillation

English

If f is a function from E to F and x is a point in E, then the oscillation of f at x computed with respect to the whole space E equals the global oscillation at x.

Русский

Пусть f: E → F, и x ∈ E. Осцилляция f в точке x по всей области равна гамильтониевой осцилляции в самой точке x: osc(f, x) = oscillationWithin f univ x.

LaTeX

$$$\\operatorname{oscillationWithin}(f,\\mathrm{univ},x)=\\operatorname{oscillation}(f,x)$$$

Lean4

/-- The oscillation of `f` at `x` within `univ` is equal to `oscillation f x` -/
theorem oscillationWithin_univ_eq_oscillation [TopologicalSpace E] (f : E → F) (x : E) :
    oscillationWithin f univ x = oscillation f x :=
  oscillationWithin_nhds_eq_oscillation f univ x Filter.univ_mem

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