Theorems · Theorem · general topology

IsCompact.uniform_oscillationWithin

∀ {E : Type u} {F : Type v} [inst : PseudoEMetricSpace F] [inst_1 : PseudoEMetricSpace E] {K : Set E} {f : E → F}
  {D : Set E} {ε : ENNReal},
  IsCompact K →
    (∀ x ∈ K, oscillationWithin f D x < ε) →
      ∃ δ > 0, ∀ x ∈ K, Metric.ediam (f '' (Metric.eball x (ENNReal.ofReal δ) ∩ D)) ≤ ε

If oscillationWithin f D x < ε at every x in a compact set K, then there exists δ > 0 such that the oscillation of f on ball x δ ∩ D is less than ε for every x in K.

Defined in

Mathlib.Analysis.Oscillation

Cited by

2 results in Mathlib

Foundations

Depth 152 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoEMetricSpacePseudoEMetricSpace