English
Equivalence of UniformEquicontinuousOn to a condition on the uniformity of α and the product of S.
Русский
Эквивалентность UniformEquicontinuousOn условию на униформность пространства α и произведение S.
LaTeX
$$$\forall F,S, UniformEquicontinuousOn(F,S) \iff \text{(uniformity α) entourages with S-projections}$$
Lean4
/-- A family `F : ι → β → α` of functions between uniform spaces is
*uniformly equicontinuous on `S : Set β`* if, for all entourages `U ∈ 𝓤 α`, there is a relative
entourage `V ∈ 𝓤 β ⊓ 𝓟 (S ×ˢ S)` such that, whenever `x` and `y` are `V`-close, we have that,
*for all `i : ι`*, `F i x` is `U`-close to `F i y`. -/
def UniformEquicontinuousOn (F : ι → β → α) (S : Set β) : Prop :=
∀ U ∈ 𝓤 α, ∀ᶠ xy : β × β in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ∀ i, (F i xy.1, F i xy.2) ∈ U
