uniformEquicontinuousOn_iff_right

English

With HasBasis for the uniformity on α on the right, UniformEquicontinuousOn F S is equivalent to a right-basis characterization via eventual behavior on 𝓤 β ⊓ 𝓟 (S×S).

Русский

С базисом справа для равномерности на α, UniformEquicontinuousOn F S эквивалентно правому базисному описанию через поведение на 𝓤 β ⊓ 𝓟 (S×S).

LaTeX

$$$\\operatorname{UniformEquicontinuousOn} F S \\iff \\forall k, p k → ∀ i, (F i x, F i y) \in s k$ для всех $(x,y)$ из пары, когда в 𝓤 β ⊓ 𝓟 (S×S).$$

Lean4

theorem uniformEquicontinuousOn_iff_right {p : κ → Prop} {s : κ → Set (α × α)} {F : ι → β → α} {S : Set β}
    (hα : (𝓤 α).HasBasis p s) :
    UniformEquicontinuousOn F S ↔ ∀ k, p k → ∀ᶠ xy : β × β in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ∀ i, (F i xy.1, F i xy.2) ∈ s k :=
  by
  rw [uniformEquicontinuousOn_iff_uniformContinuousOn, UniformContinuousOn,
    (UniformFun.hasBasis_uniformity_of_basis ι α hα).tendsto_right_iff]
  rfl

Похожие утверждения