tendsto_iff_tendstoUniformlyOn — Mathlib

English

Equivalent reformulation of tendsto with respect to TendstoUniformlyOn on sets S.

Русский

Эквивалентная формулировка сходимости через TendstoUniformlyOn на множествах S.

LaTeX

$$$$ \text{Tendsto}(a,p,nhds(a_0)) \iff \forall s \in \mathfrak{S},\ TendstoUniformlyOn(\ldots, p, s). $$$$

Lean4

theorem tendsto_iff_tendstoUniformlyOn {ι : Type*} {p : Filter ι} [UniformSpace F] [IsUniformAddGroup F]
    (𝔖 : Set (Set E)) {a : ι → UniformConvergenceCLM σ F 𝔖} {a₀ : UniformConvergenceCLM σ F 𝔖} :
    Filter.Tendsto a p (𝓝 a₀) ↔ ∀ s ∈ 𝔖, TendstoUniformlyOn (a · ·) a₀ p s :=
  by
  rw [(isEmbedding_coeFn σ F 𝔖).tendsto_nhds_iff, UniformOnFun.tendsto_iff_tendstoUniformlyOn]
  rfl

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