tendstoLocallyUniformlyOn_finsetRange

English

If h is HasProdLocallyUniformlyOn f g s, then TendstoLocallyUniformlyOn with Finset.range range converges on s.

Русский

Если h = HasProdLocallyUniformlyOn f g s, тогда TendstoLocallyUniformlyOn с диапазона Finset.range сходится на s.

LaTeX

$$$ (h : HasProdLocallyUniformlyOn f g s) \Rightarrow TendstoLocallyUniformlyOn (\lambda N b. (Finset.range N).prod (λ i, f i b)) g atTop s $$$

Lean4

@[to_additive]
theorem tendstoLocallyUniformlyOn_finsetRange {f : ℕ → β → α} (h : HasProdLocallyUniformlyOn f g s) :
    TendstoLocallyUniformlyOn (fun N b ↦ ∏ i ∈ Finset.range N, f i b) g atTop s :=
  by
  rw [hasProdLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn] at h
  intro v hv r hr
  obtain ⟨t, ht, htr⟩ := h v hv r hr
  exact ⟨t, ht, Filter.tendsto_finset_range.eventually htr⟩

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