English
Uniform continuity on s is characterized by the ≤-version: for every ε > 0 there exists δ > 0 such that dist x y ≤ δ implies dist(f x) f y ≤ ε for x,y ∈ s.
Русский
Уравномеренная непрерывность на s эквивалентна версии с ≤: для каждого ε>0 существует δ>0 такое, что dist(x,y) ≤ δ ⇒ dist(f(x),f(y)) ≤ ε для x,y ∈ s.
LaTeX
$$$$ \text{UniformContinuousOn}(f,s) \iff \forall \varepsilon > 0, \exists \delta > 0, \forall x \in s, \forall y \in s, \operatorname{dist}(x,y) \le \delta \Rightarrow \operatorname{dist}(f(x),f(y)) \le \varepsilon. $$$$
Lean4
theorem uniformContinuousOn_iff_le [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_le.uniformContinuousOn_iff Metric.uniformity_basis_dist_le
