English
For a function f: α → G into a complete group G, Multipliable f is equivalent to Tendsto f to cofinite at 1.
Русский
Для функции f: α → G в полный элемент G умножимость равна стремлению f к единице по кофинитному фильтру.
LaTeX
$$$\\displaystyle \\text{Multipliable}(f) \\iff \\text{Tendsto}(f,\\text{cofinite},(\\mathcal{nhds} 1))$$$
Lean4
/-- Let `G` be a complete nonarchimedean multiplicative abelian group, and let `f : α → G` be a
function that tends to one on the filter of cofinite sets. Then `f` is unconditionally
multipliable. -/
@[to_additive /-- Let `G` be a complete nonarchimedean additive abelian group, and let `f : α → G`
be a function that tends to zero on the filter of cofinite sets. Then `f` is unconditionally
summable. -/
]
theorem multipliable_of_tendsto_cofinite_one [CompleteSpace G] {f : α → G} (hf : Tendsto f cofinite (𝓝 1)) :
Multipliable f :=
CompleteSpace.complete (cauchySeq_prod_of_tendsto_cofinite_one hf)
