English
If the uniformity on β has HasBasis p s, then UniformEquicontinuous F holds iff for every basis index k with p k the uniform closeness (F i x, F i y) ∈ U holds for all i for bunched pairs (x,y) in s k.
Русский
Если равномерность на β имеет HasBasis p s, то UniformEquicontinuous F эквивалентно тому, что для каждого индекса базы k с p k параблизованных элементов x,y в s k удовлетворяет нужной близости для всех i.
LaTeX
$$$\\operatorname{UniformEquicontinuous} F \\iff \\forall k, p k \\to \\forall i, (F i x, F i y) \\in U$ для всех (x,y)∈ s k и U в 𝓤 α.$$
Lean4
theorem uniformEquicontinuous_iff_left {p : κ → Prop} {s : κ → Set (β × β)} {F : ι → β → α} (hβ : (𝓤 β).HasBasis p s) :
UniformEquicontinuous F ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x y, (x, y) ∈ s k → ∀ i, (F i x, F i y) ∈ U :=
by
rw [uniformEquicontinuous_iff_uniformContinuous, UniformContinuous,
hβ.tendsto_iff (UniformFun.hasBasis_uniformity ι α)]
simp only [Prod.forall]
rfl
