English
If oscillationWithin f D x is less than ε for every x in a compact K, then there exists a universal δ>0 such that for all x in K, the oscillation of f on ball x(δ) ∩ D is less than ε.
Русский
Если для всех x∈K выполнено oscillationWithin f D x < ε, где K компактно, то существует δ>0 такое, что для всех x∈K осцилляция f на B(x,δ) ∩ D < ε.
LaTeX
$$$\\forall x\\in K,\\ \\operatorname{oscillationWithin}(f,D,x)<\\varepsilon \\Rightarrow \\exists \\delta>0, \\forall x\\in K,\\ \\operatorname{diam}(f''(\\ball{x}{\\delta}\\cap D))\\le \\varepsilon$$$
Lean4
/-- 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`. -/
theorem uniform_oscillation {K : Set E} (comp : IsCompact K) {f : E → F} {ε : ENNReal}
(hK : ∀ x ∈ K, oscillation f x < ε) : ∃ δ > 0, ∀ x ∈ K, diam (f '' (ball x (ENNReal.ofReal δ))) ≤ ε :=
by
simp only [← oscillationWithin_univ_eq_oscillation] at hK
convert ← comp.uniform_oscillationWithin hK
exact inter_univ _
