English
ε-δ characterization of uniform continuity on a set in pseudo-emetric spaces: UniformContinuousOn f s iff for every ε > 0 there exists δ > 0 such that for all a,b ∈ s with edist(a,b) < δ, we have edist(f a, f b) < ε.
Русский
Характеризация ε-δ равномерной непрерывности на подмножестве в псевдоэмитическом пространстве: UniformContinuousOn f s эквивалentно тому, что для любого ε>0 существует δ>0 такое, что для любых a,b∈s с edist(a,b) < δ следует edist(f a, f b) < ε.
LaTeX
$$$ UniformContinuousOn(f,s) \iff \forall \varepsilon>0,\ \exists \delta>0,\ \forall a\in s,\ \forall b\in s,\ edist(a,b) < \delta\ \Rightarrow\ edist(f(a),f(b)) < \varepsilon. $$$
Lean4
/-- ε-δ characterization of uniform continuity on a set for pseudoemetric spaces -/
theorem uniformContinuousOn_iff [PseudoEMetricSpace β] {f : α → β} {s : Set α} :
UniformContinuousOn f s ↔ ∀ ε > 0, ∃ δ > 0, ∀ {a}, a ∈ s → ∀ {b}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε :=
uniformity_basis_edist.uniformContinuousOn_iff uniformity_basis_edist
