nat_tprod_vanishing — Mathlib

English

If f: ℕ → G is multipliable, then the tail products tend to the identity; more precisely, Tendsto (fun i => ∏' k, f(k+i)) atTop (𝓝 1).

Русский

Если f: ℕ → G мультиплируемо, хвостовые произведения сходятся к единице: Tendsto (i ↦ ∏' k, f(k+i)) при i → ∞ к 1.

LaTeX

$$$\text{Tendsto}\_{i \to \mathrm{atTop}}\left(\prod' k, f(k+i)\right) = 1$$$

Lean4

@[to_additive]
theorem nat_tprod_vanishing {f : ℕ → G} (hf : Multipliable f) ⦃e : Set G⦄ (he : e ∈ 𝓝 1) :
    ∃ N : ℕ, ∀ t ⊆ {n | N ≤ n}, (∏' n : t, f n) ∈ e :=
  letI : UniformSpace G := IsTopologicalGroup.toUniformSpace G
  have : IsUniformGroup G := isUniformGroup_of_commGroup
  cauchySeq_finset_iff_nat_tprod_vanishing.1 hf.hasProd.cauchySeq e he

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