oscillation — Mathlib

English

The oscillation of a function f at a point is the infimum over all sets S in neighborhoods of the point of the diameter of S under f.

Русский

Осцилляция функции f в точке x есть инфимум диаметра образов множеств S под действием f, где S варьируется по окрестностям x.

LaTeX

$$$\\operatorname{oscillation}(f,x) = \\inf\\{\\operatorname{diam}(S): S\\in\\mathcal{N}(x)\\},$ (in the sense of the provided definition).$$

Lean4

/-- The oscillation of `f : E → F` at `x`. -/
noncomputable def oscillation [TopologicalSpace E] (f : E → F) (x : E) : ENNReal :=
  ⨅ S ∈ (𝓝 x).map f, diam S

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