English
For f : α → β between pseudo metric spaces, f is uniformly continuous if and only if for every ε > 0 there exists δ > 0 such that dist a b < δ implies dist(f a) (f b) < ε.
Русский
Для отображения f : α → β между псевдометрическими пространствами f будет равномерно непрерывно тогда и только тогда, когда для любого ε > 0 существует δ > 0 такое, что dist(a,b) < δ ⇒ dist(f a, f b) < ε.
LaTeX
$$$$ \text{UniformContinuous}(f) \iff \forall \varepsilon > 0, \exists \delta > 0, \forall a,b, \operatorname{dist}(a,b) < \delta \Rightarrow \operatorname{dist}(f(a),f(b)) < \varepsilon. $$$$
Lean4
theorem uniformContinuous_iff [PseudoMetricSpace β] {f : α → β} :
UniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃a b : α⦄, dist a b < δ → dist (f a) (f b) < ε :=
uniformity_basis_dist.uniformContinuous_iff uniformity_basis_dist
