Theorems · Theorem · general topology

IsCompact.uniform_oscillation

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

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

Defined in

Mathlib.Analysis.Oscillation

Cited by

0 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpacePseudoEMetricSpace