tendstoUniformlyOn_iff_seq_tendstoUniformlyOn

English

Let l be a countably generated filter. Then TendstoUniformlyOn F f l s holds iff for every sequence u: ℕ → ι with Tendsto u atTop l, TendstoUniformlyOn (fun n => F (u n)) f atTop s.

Русский

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

LaTeX

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

Lean4

theorem tendstoUniformlyOn_iff_seq_tendstoUniformlyOn {l : Filter ι} [l.IsCountablyGenerated] :
    TendstoUniformlyOn F f l s ↔ ∀ u : ℕ → ι, Tendsto u atTop l → TendstoUniformlyOn (fun n => F (u n)) f atTop s :=
  ⟨TendstoUniformlyOn.seq_tendstoUniformlyOn, tendstoUniformlyOn_of_seq_tendstoUniformlyOn⟩

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