English
Multipliability of f is equivalent to vanishing of tail products: for every neighborhood of 1 there exists a finite set after which all tail products lie in that neighborhood.
Русский
Умножаемость f эквивалентна исчезновению хвостовых произведений: для любой окрестности 1 существует конечное множество, после которого хвостовые произведения лежат внутри этой окрестности.
LaTeX
$$$\operatorname{Multipliable}(f) \iff \forall e \in \mathcal{N}(1), \exists s, \forall t, \text{Disjoint}(t,s) \Rightarrow (\prod_{b\in t} f(b)) \in e.$$$
Lean4
@[to_additive]
theorem multipliable_iff_tprod_vanishing :
Multipliable f ↔ ∀ e ∈ 𝓝 (1 : α), ∃ s : Finset β, ∀ t : Set β, Disjoint t s → (∏' b : t, f b) ∈ e := by
rw [multipliable_iff_cauchySeq_finset, cauchySeq_finset_iff_tprod_vanishing]
-- TODO: generalize to monoid with a uniform continuous subtraction operator: `(a + b) - b = a`
