English
Equivalence of UniformEquicontinuousOn with respect to left and right basis data: the pair of HasBasis data is sufficient to characterize uniform equicontinuity.
Русский
Эквивалентоность UniformEquicontinuousOn относительно левого и правого набора баз данных: данные двух баз достаточны для характеристики равномерной экквинтоентности.
LaTeX
$$$\\operatorname{UniformEquicontinuousOn} F S \\iff \\text{HasBasis data on both sides yield the equivalence.}$$$
Lean4
theorem uniformEquicontinuousOn_iff {κ₁ κ₂ : Type*} {p₁ : κ₁ → Prop} {s₁ : κ₁ → Set (β × β)} {p₂ : κ₂ → Prop}
{s₂ : κ₂ → Set (α × α)} {F : ι → β → α} {S : Set β} (hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p₁ s₁)
(hα : (𝓤 α).HasBasis p₂ s₂) :
UniformEquicontinuousOn F S ↔ ∀ k₂, p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x y, (x, y) ∈ s₁ k₁ → ∀ i, (F i x, F i y) ∈ s₂ k₂ :=
by
rw [uniformEquicontinuousOn_iff_uniformContinuousOn, UniformContinuousOn,
hβ.tendsto_iff (UniformFun.hasBasis_uniformity_of_basis ι α hα)]
simp only [Prod.forall]
rfl
