English
A function f: α → β is uniformly continuous on a set S ⊆ α if the usual diagonal- closeness condition holds only for pairs from S × S.
Русский
Функция f: α → β равномерно непрерывна на подмножестве S ⊆ α, если условие близости по диагонали выполняется только для пар из S × S.
LaTeX
$$$\text{UniformContinuousOn}(f,S)\;\text{is defined by}\; \text{Tendsto}\big( (x,y)\mapsto (f x, f y) \big) (\mathcal{U} α \sqcap \mathcal{P}(S\times S)) (\mathcal{U} β).$$$
Lean4
/-- A function `f : α → β` is *uniformly continuous* on `s : Set α` if `(f x, f y)` tends to
the diagonal as `(x, y)` tends to the diagonal while remaining in `s ×ˢ s`.
In other words, if `x` is sufficiently close to `y`, then `f x` is close to
`f y` no matter where `x` and `y` are located in `s`. -/
def UniformContinuousOn [UniformSpace β] (f : α → β) (s : Set α) : Prop :=
Tendsto (fun x : α × α => (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (s ×ˢ s)) (𝓤 β)
