tendstoUniformlyOn_of_tendsto — Mathlib

English

Criterion for TendstoUniformly to hold globally in terms of uniformity basis.

Русский

Критерий существования TendstoUniformly в терминах базиса униформности.

LaTeX

$$$TendstoUniformly F f l \iff \forall i, pβ i \rightarrow \forall x, (f x, F n x) \in sβ i \text{ eventually in } l$$$

Lean4

/-- A uniformly Cauchy sequence converges uniformly to its limit -/
theorem tendstoUniformlyOn_of_tendsto (hF : UniformCauchySeqOn F p s)
    (hF' : ∀ x : α, x ∈ s → Tendsto (fun n => F n x) p (𝓝 (f x))) : TendstoUniformlyOn F f p s :=
  tendstoUniformlyOn_iff_tendstoUniformlyOnFilter.mpr
    (hF.uniformCauchySeqOnFilter.tendstoUniformlyOnFilter_of_tendsto hF')

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