English
If the left HasBasis for β is given, UniformEquicontinuousOn F S is equivalent to a left-basis criterion via an infimum of 𝓤 β and 𝓟 (S×S).
Русский
При наличии левого базиса для β UniformEquicontinuousOn F S эквивалентно левому базису через инфиминуцию 𝓤 β и 𝓟 (S×S).
LaTeX
$$$\\operatorname{UniformEquicontinuousOn} F S \\iff \\forall k, p k → \\forall (x,y) ∈ s k, ∀ i, (F i x, F i y) ∈ U$ для U из базиса.$$
Lean4
theorem uniformEquicontinuous_iff {κ₁ κ₂ : Type*} {p₁ : κ₁ → Prop} {s₁ : κ₁ → Set (β × β)} {p₂ : κ₂ → Prop}
{s₂ : κ₂ → Set (α × α)} {F : ι → β → α} (hβ : (𝓤 β).HasBasis p₁ s₁) (hα : (𝓤 α).HasBasis p₂ s₂) :
UniformEquicontinuous F ↔ ∀ k₂, p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x y, (x, y) ∈ s₁ k₁ → ∀ i, (F i x, F i y) ∈ s₂ k₂ :=
by
rw [uniformEquicontinuous_iff_uniformContinuous, UniformContinuous,
hβ.tendsto_iff (UniformFun.hasBasis_uniformity_of_basis ι α hα)]
simp only [Prod.forall]
rfl
