uniform_continuity — Mathlib

English

Every continuous map f: α→β from a compact space α is uniformly continuous; there exists δ>0 for every ε>0 such that dist(f(x),f(y))<ε whenever dist(x,y)<δ.

Русский

Для непрерывного отображения f: α→β, если α компактно, то оно равномерно непрерывно: существует δ>0, что расстояние изображений меньше ε при расстоянии аргументов менее δ.

LaTeX

$$$\forall f:C(α,β), ∀ε>0, ∃δ>0: ∀x,y, dist(x,y)<δ \Rightarrow dist(f(x),f(y))<ε$$$

Lean4

theorem uniform_continuity (f : C(α, β)) (ε : ℝ) (h : 0 < ε) : ∃ δ > 0, ∀ {x y}, dist x y < δ → dist (f x) (f y) < ε :=
  Metric.uniformContinuous_iff.mp (CompactSpace.uniformContinuous_of_continuous f.continuous) ε h

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