English
An analogue of the HasBasis tendsto_iff for TendstoUniformlyOnFilter: TendstoUniformlyOnFilter F f l l' is equivalent to a basis-based condition on all indices i in the basis.
Русский
Аналог HasBasis для TendstoUniformlyOnFilter: TendstoUniformlyOnFilter F f l l' эквивалентно условию, основанному на базисе по всем индексам i.
LaTeX
$$$TendstoUniformlyOnFilter F f l l' \iff \forall i,\ pβ i \rightarrow \forallᶠ n \in l \times\! l',\ (f n.2, F n.1 n.2) \in sβ i$$$
Lean4
/-- An analogue of `Filter.HasBasis.tendsto_iff` for `TendstoUniformlyOnFilter`. -/
theorem tendstoUniformlyOnFilter_iff {F : X → α → β} {f : α → β} {l : Filter X} {l' : Filter α} {pX : ιX → Prop}
{sX : ιX → Set X} {pα : ια → Prop} {sα : ια → Set α} {pβ : ιβ → Prop} {sβ : ιβ → Set (β × β)}
(hl : l.HasBasis pX sX) (hl' : l'.HasBasis pα sα) (hβ : (uniformity β).HasBasis pβ sβ) :
TendstoUniformlyOnFilter F f l l' ↔
(∀ i, pβ i → ∃ j k, (pX j ∧ pα k) ∧ ∀ x a, x ∈ sX j → a ∈ sα k → (f a, F x a) ∈ sβ i) :=
by simp [hβ.tendstoUniformlyOnFilter_iff_of_uniformity, (hl.prod hl').eventually_iff]
