English
A function f: α → β is uniformly continuous on a set s ⊆ α if and only if for every ε > 0 there exists δ > 0 such that for all x,y ∈ s with dist x y < δ we have dist(f x) f y < ε.
Русский
Функция f: α → β равномерно непрерывна на области s ⊆ α, если и только если для любого ε>0 существует δ>0 такое, что для всех x,y ∈ s с dist(x,y) < δ выполняется dist(f(x), f(y)) < ε.
LaTeX
$$$$ \text{UniformContinuousOn}(f,s) \iff \forall \varepsilon > 0, \exists \delta > 0, \forall x \in s, \forall y \in s, \operatorname{dist}(x,y) < \delta \Rightarrow \operatorname{dist}(f(x),f(y)) < \varepsilon. $$$$
Lean4
theorem uniformContinuousOn_iff [PseudoMetricSpace β] {f : α → β} {s : Set α} :
UniformContinuousOn f s ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y < δ → dist (f x) (f y) < ε :=
Metric.uniformity_basis_dist.uniformContinuousOn_iff Metric.uniformity_basis_dist
