English
Let both the left and right HasBasis be present for β and α, respectively. Then UniformEquicontinuous F is equivalent to a basis-driven condition relating all i and x,y via the product basis s1 and s2.
Русский
Пусть обе базы имеются; тогда UniformEquicontinuous F эквивалентно базисному условию, связывающему все i и пары x,y через базы s1 и s2.
LaTeX
$$$\\operatorname{UniformEquicontinuous} F \\iff \\forall k_2, p_2 k_2 → \\exists k_1, p_1 k_1 ∧ \\forall x,y, (x,y) ∈ s_1 k_1 → \\forall i, (F i x, F i y) ∈ s_2 k_2.$$$
Lean4
theorem uniformEquicontinuous_iff_right {p : κ → Prop} {s : κ → Set (α × α)} {F : ι → β → α} (hα : (𝓤 α).HasBasis p s) :
UniformEquicontinuous F ↔ ∀ k, p k → ∀ᶠ xy : β × β in 𝓤 β, ∀ i, (F i xy.1, F i xy.2) ∈ s k :=
by
rw [uniformEquicontinuous_iff_uniformContinuous, UniformContinuous,
(UniformFun.hasBasis_uniformity_of_basis ι α hα).tendsto_right_iff]
rfl
