English
An analogue of the right-criterion for TendstoUniformlyOnFilter with a uniformity basis: TendstoUniformlyOn F f l l' is equivalent to a basis-driven condition identical in form to the standard HasBasis rule.
Русский
Аналог правого критерия для TendstoUniformlyOnFilter с базисом униформности: TendstoUniformlyOn F f l l' эквивалентно условию на основе базиса, аналогичному обычному правилу HasBasis.
LaTeX
$$$TendstoUniformlyOn F f l l' \iff \forall i,\ pβ i \rightarrow \exists j,k,\ (pX j \wedge pα k) \wedge \forall x,a,\ x \in sX j \to a \in sα k \to (f a, F x a) \in sβ i$$$
Lean4
/-- An analogue of `Filter.HasBasis.tendsto_right_iff` for `TendstoUniformlyOn`. -/
theorem tendstoUniformlyOn_iff_of_uniformity {F : X → α → β} {f : α → β} {l : Filter X} {s : Set α} {pβ : ιβ → Prop}
{sβ : ιβ → Set (β × β)} (hβ : (uniformity β).HasBasis pβ sβ) :
TendstoUniformlyOn F f l s ↔ (∀ i, pβ i → ∀ᶠ n in l, ∀ x ∈ s, (f x, F n x) ∈ sβ i) := by
simp_rw [tendstoUniformlyOn_iff_tendsto, hβ.tendsto_right_iff, eventually_prod_principal_iff]
