English
A function f is uniformly continuous iff for every ε > 0 there exists δ > 0 such that edist(a,b) < δ implies edist(f a, f b) < ε for all a,b.
Русский
Функция f равномерно непрерывна тогда и только тогда, когда для каждого ε>0 существует δ>0 такое, что edist(a,b) < δ влечет edist(f a, f b) < ε для всех a,b.
LaTeX
$$$ UniformContinuous(f) \iff \forall \varepsilon>0,\ \exists \delta>0,\ \forall a,b,\ edist(a,b) < \delta \Rightarrow edist(f(a),f(b)) < \varepsilon. $$$
Lean4
/-- ε-δ characterization of uniform continuity on pseudoemetric spaces -/
theorem uniformContinuous_iff [PseudoEMetricSpace β] {f : α → β} :
UniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, edist a b < δ → edist (f a) (f b) < ε :=
uniformity_basis_edist.uniformContinuous_iff uniformity_basis_edist
