English
Under the same hypotheses, there exists a finite S such that for all disjoint finite t, the tail product ∏' b : t, f b lies in e.
Русский
При тех же предположениях существует конечное множество S, такое что для любых Disjoint(t, S) бесконечное произведение по t лежит в e.
LaTeX
$$$$\\exists s \\in \\mathrm{Finset}(\\beta), \\forall t \\subseteq \\beta, \\mathrm{Disjoint}(t,s) \\Rightarrow \\prod' b \\in t, f(b) \\in e.$$$$
Lean4
@[to_additive]
theorem tprod_vanishing (hf : Multipliable f) ⦃e : Set G⦄ (he : e ∈ 𝓝 1) :
∃ s : Finset α, ∀ t : Set α, Disjoint t s → (∏' b : t, f b) ∈ e := by
classical
letI : UniformSpace G := IsTopologicalGroup.toUniformSpace G
have : IsUniformGroup G := isUniformGroup_of_commGroup
exact cauchySeq_finset_iff_tprod_vanishing.1 hf.hasProd.cauchySeq e he
