oscillationWithin — Mathlib

English

Oscillation within a subset D is the infimum over the images of D under f of their diameters, taken over sets in the neighborhood filter of x restricted to D.

Русский

Осцилляция внутри множества D равна инфимума над образами D при f диаметров этих образов, в редуцированной окрестности x.

LaTeX

$$$\\operatorname{oscillationWithin}(f,D,x) = \\inf\\{\\operatorname{diam}(S): S\\in (\\mathcal{N}(x)\\text{ restricted to }D)\\text{ image under }f\\}$$$

Lean4

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

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