English
For a Multipliable f: α → G into a topological group G, for every neighborhood e of the identity 1, there exists a finite set S such that for every finite t disjoint from S, the product over t lies in e.
Русский
Для суммируемой функции f: α → G в топологической группе G, для каждого окрестности e(1) существует конечное множество S, такое что для каждого конечного множества t, попадающего в дополнение S, произведение по t лежит в e.
LaTeX
$$$$\\forall e \\in \\mathcal{N}(1), \\exists S \\in \\mathrm{Finset}(\\alpha), \\forall t \\in \\mathcal{P}_{fin}(\\alpha), \\mathrm{Disjoint}(t,S) \\Rightarrow \\prod_{k\\in t} f(k) \\in e.$$$$
Lean4
@[to_additive]
theorem vanishing (hf : Multipliable f) ⦃e : Set G⦄ (he : e ∈ 𝓝 (1 : G)) :
∃ s : Finset α, ∀ t, Disjoint t s → (∏ k ∈ t, f k) ∈ e := by
classical
letI : UniformSpace G := IsTopologicalGroup.toUniformSpace G
have : IsUniformGroup G := isUniformGroup_of_commGroup
exact cauchySeq_finset_iff_prod_vanishing.1 hf.hasProd.cauchySeq e he
