English
An analogue of the Filter.HasBasis tendsto_iff for TendstoUniformlyOn: the same HasBasis pattern translates to TendstoUniformlyOn.
Русский
Аналог фильтра HasBasis tendsto_iff для TendstoUniformlyOn: тот же образец HasBasis переносится на TendstoUniformlyOn.
LaTeX
$$$TendstoUniformlyOn F f l s \iff \forall i,\ pβ i \rightarrow \exists j,\ pX j \wedge \forall x \in sX j, \forall a \in s,\ (f a, F x a) \in sβ i$$$
Lean4
/-- An analogue of `Filter.HasBasis.tendsto_iff` for `TendstoUniformlyOn`. -/
theorem tendstoUniformlyOn_iff {F : X → α → β} {f : α → β} {l : Filter X} {s : Set α} {pX : ιX → Prop} {sX : ιX → Set X}
{pβ : ιβ → Prop} {sβ : ιβ → Set (β × β)} (hl : l.HasBasis pX sX) (hβ : (uniformity β).HasBasis pβ sβ) :
TendstoUniformlyOn F f l s ↔ (∀ i, pβ i → ∃ j, pX j ∧ ∀ ⦃x⦄, x ∈ sX j → ∀ a ∈ s, (f a, F x a) ∈ sβ i) := by
simp [hβ.tendstoUniformlyOn_iff_of_uniformity, hl.eventually_iff]
