tendstoUniformly_iff_of_uniformity

English

The uniform convergence statement TendstoUniformly is equivalent to a pointwise statement of convergence of each F n to the limit uniformly across the index set.

Русский

Утверждение равномерной сходимости TendstoUniformly эквивалентно по точкам: для каждого n сходится равномерно на индексах.

LaTeX

$$$TendstoUniformly F f l \iff \forall x, Tendsto (\lambda n. F n x) l (\ nhds (f x))$$$

Lean4

/-- An analogue of `Filter.HasBasis.tendsto_right_iff` for `TendstoUniformly`. -/
theorem tendstoUniformly_iff_of_uniformity {F : X → α → β} {f : α → β} {l : Filter X} {pβ : ιβ → Prop}
    {sβ : ιβ → Set (β × β)} (hβ : (uniformity β).HasBasis pβ sβ) :
    TendstoUniformly F f l ↔ (∀ i, pβ i → ∀ᶠ n in l, ∀ x, (f x, F n x) ∈ sβ i) := by
  simp_rw [← tendstoUniformlyOn_univ, hβ.tendstoUniformlyOn_iff_of_uniformity, mem_univ, true_imp_iff]

Похожие утверждения