English
If f is unconditionally multipliable, then f(a) tends to 1 along the cofinite filter on α.
Русский
Если f является безусловно множимым, то f(a) стремится к единице вдоль кофинитного фильтра на α.
LaTeX
$$$$ \operatorname{Tendsto} f \; \mathrm{cofinite} \; (\mathcal{N} 1) $$$$
Lean4
/-- Product divergence test: if `f` is unconditionally multipliable, then `f x` tends to one along
`cofinite`. -/
@[to_additive /-- Series divergence test: if `f` is unconditionally summable, then `f x` tends to
zero along `cofinite`. -/
]
theorem tendsto_cofinite_one (hf : Multipliable f) : Tendsto f cofinite (𝓝 1) :=
by
intro e he
rw [Filter.mem_map]
rcases hf.vanishing he with ⟨s, hs⟩
refine s.eventually_cofinite_notMem.mono fun x hx ↦ ?_
· simpa using hs { x } (disjoint_singleton_left.2 hx)
