English
If the infimum of uniformities (min) has a HasBasis, then UniformEquicontinuousOn F S is equivalent to a basis-driven condition involving that HasBasis.
Русский
Если у объединенной инфиминформированной равномерности есть база, то UniformEquicontinuousOn F S эквивалентно условию с этой базой.
LaTeX
$$$\\operatorname{UniformEquicontinuousOn} F S \\iff \\forall U \\in \\bigl\\text{min}(\\mathcal{U}_{β}, \\text{principal}(S\\times S)) , \\exists k, p k ∧ \\forall x,y: (x,y)∈ s k → \\forall i, (F i x, F i y) ∈ U.$$$
Lean4
theorem uniformEquicontinuousOn_iff_left {p : κ → Prop} {s : κ → Set (β × β)} {F : ι → β → α} {S : Set β}
(hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p s) :
UniformEquicontinuousOn F S ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x y, (x, y) ∈ s k → ∀ i, (F i x, F i y) ∈ U :=
by
rw [uniformEquicontinuousOn_iff_uniformContinuousOn, UniformContinuousOn,
hβ.tendsto_iff (UniformFun.hasBasis_uniformity ι α)]
simp only [Prod.forall]
rfl
