tendstoUniformly_iff_seq_tendstoUniformly

English

Let l be countably generated. Then TendstoUniformly F f l iff for all u: ℕ → ι with Tendsto u atTop l, TendstoUniformly (λ n. F (u n)) f atTop.

Русский

Пусть l счётно порожден. Тогда TendstoUniformly F f l эквивалентно тому, что для каждой последовательности u: ℕ → ι с Tendsto u atTop l выполняется TendstoUniformly (F ∘ u) f atTop.

LaTeX

$$$\\text{TendstoUniformly } F f l \\;\\Longleftrightarrow\\; \\forall u:\\mathbb{N} \\to ι,\\; \\text{Tendsto } u atTop l \\to \\text{TendstoUniformly } (\\lambda n. F (u n)) f atTop$$$

Lean4

theorem tendstoUniformly_iff_seq_tendstoUniformly {l : Filter ι} [l.IsCountablyGenerated] :
    TendstoUniformly F f l ↔ ∀ u : ℕ → ι, Tendsto u atTop l → TendstoUniformly (fun n => F (u n)) f atTop :=
  by
  simp_rw [← tendstoUniformlyOn_univ]
  exact tendstoUniformlyOn_iff_seq_tendstoUniformlyOn

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