multipliable_iff_nat_tprod_vanishing

English

If f: ℕ → G is multipliable, then for every neighborhood e of 1 in G there exists N such that for all t ⊆ {n ≥ N}, the finite tail product ∏' n ∈ t, f n lies in e.

Русский

Если f: ℕ → G мультиплируемо, то для любого окрестности e точки 1 в G существует N, так что для всех подмножеств t, содержащих элементы n ≥ N, хвостовое произведение ∏' n ∈ t, f(n) принадлежит e.

LaTeX

$$$\exists N\;\forall t\subseteq\{n\mid N\le n\},\; \prod' n\in t, f(n) \in e$$$

Lean4

@[to_additive]
theorem multipliable_iff_nat_tprod_vanishing {f : ℕ → G} :
    Multipliable f ↔ ∀ e ∈ 𝓝 1, ∃ N : ℕ, ∀ t ⊆ {n | N ≤ n}, (∏' n : t, f n) ∈ e := by
  rw [multipliable_iff_cauchySeq_finset, cauchySeq_finset_iff_nat_tprod_vanishing]

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