English
A variant of TendstoUniformlyOn with a uniformity basis: TendstoUniformlyOn F f l s is equivalent to a basis-driven eventual condition over s.
Русский
Вариант TendstoUniformlyOn с базисом униформности: TendstoUniformlyOn F f l s эквивалентно базисному условию, выполняющемуся позднее в s.
LaTeX
$$$TendstoUniformlyOn F f l s \iff \forall i,\ pβ i \rightarrow \forall x\in s, \forall a\in s,\ (f a, F x a) \in sβ i$$$
Lean4
/-- An analogue of `Filter.HasBasis.tendsto_iff` for `TendstoUniformly`. -/
theorem tendstoUniformly_iff {F : X → α → β} {f : α → β} {l : Filter X} {pX : ιX → Prop} {sX : ιX → Set X}
(hl : l.HasBasis pX sX) {pβ : ιβ → Prop} {sβ : ιβ → Set (β × β)} (hβ : (uniformity β).HasBasis pβ sβ) :
TendstoUniformly F f l ↔ (∀ i, pβ i → ∃ j, pX j ∧ ∀ ⦃x⦄, x ∈ sX j → ∀ a, (f a, F x a) ∈ sβ i) := by
simp only [hβ.tendstoUniformly_iff_of_uniformity, hl.eventually_iff]
