uniformContinuous_iff_eventually — Mathlib

English

Uniform continuity is equivalent to always having (f x1, f x2) ∈ r eventually for all r in the target uniformity when sampling x1, x2 from the domain near each other.

Русский

Униформная непрерывность эквивалентна тому, что для каждого спутника r в целевой равномерности, пары (x1,x2) близки в пределах домена, если в них выбираем x1,x2 близко друг к другу.

LaTeX

$$$ UniformContinuous f \iff \forall r \in \mathcal{U}(\beta), \forall^\infty (x,y) \in \mathcal{U}(\alpha), (f x, f y) \in r. $$$

Lean4

theorem uniformContinuous_iff_eventually [UniformSpace β] {f : α → β} :
    UniformContinuous f ↔ ∀ r ∈ 𝓤 β, ∀ᶠ x : α × α in 𝓤 α, (f x.1, f x.2) ∈ r :=
  Iff.rfl

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