English
An analogue of the right-criterion for TendstoUniformlyOnFilter using a uniformity basis: TendstoUniformlyOnFilter F f l l' holds exactly when for every index i coming from the basis, all but a small set of indices satisfy the uniform relation (f n.2, F n.1 n.2) ∈ sβ i.
Русский
Аналог правого критерия для TendstoUniformlyOnFilter с использованием базиса униформности: TendstoUniformlyOnFilter F f l l' эквивалентно тому, что для каждого индекса i из базиса практически все пары (n) удовлетворяют неравенству (f n.2, F n.1 n.2) ∈ sβ i.
LaTeX
$$$TendstoUniformlyOnFilter\ F\ f\ l\ l' \\iff \\forall i,\\ pβ i \\rightarrow \\forall^\\infty n \\in l \\times\\! l',\\ (f\,n.2,\ F\,n.1\,n.2) \\in sβ i$$$
Lean4
/-- An analogue of `Filter.HasBasis.tendsto_right_iff` for `TendstoUniformlyOnFilter`. -/
theorem tendstoUniformlyOnFilter_iff_of_uniformity {F : X → α → β} {f : α → β} {l : Filter X} {l' : Filter α}
{pβ : ιβ → Prop} {sβ : ιβ → Set (β × β)} (hβ : (uniformity β).HasBasis pβ sβ) :
TendstoUniformlyOnFilter F f l l' ↔ (∀ i, pβ i → ∀ᶠ n in l ×ˢ l', (f n.2, F n.1 n.2) ∈ sβ i) := by
rw [tendstoUniformlyOnFilter_iff_tendsto, hβ.tendsto_right_iff]
