English
If f: α → G tends to 1 along the cofinite filter, then the finite partial products ∏_{i∈s} f(i) form a Cauchy sequence in α.
Русский
Если f: α → G стремится к единице по фильтру дополнительно конечное, то частичные произведения по конечным подмножествам образуют последовательность Cauchy.
LaTeX
$$$\\displaystyle \\text{Tendsto}\\ f\\ (\\text{cofinite})\\ (\\mathcal{N}(1)) \\Rightarrow CauchySeq\\ (s \\mapsto \\prod_{i \\in s} f(i))$$$
Lean4
/-- Let `G` be a nonarchimedean multiplicative abelian group, and let `f : α → G` be a function that
tends to one on the filter of cofinite sets. For each finite subset of `α`, consider the partial
product of `f` on that subset. These partial products form a Cauchy filter. -/
@[to_additive /-- Let `G` be a nonarchimedean additive abelian group, and let `f : α → G` be a
function that tends to zero on the filter of cofinite sets. For each finite subset of `α`, consider
the partial sum of `f` on that subset. These partial sums form a Cauchy filter. -/
]
theorem cauchySeq_prod_of_tendsto_cofinite_one {f : α → G} (hf : Tendsto f cofinite (𝓝 1)) :
CauchySeq (fun s ↦ ∏ i ∈ s, f i) := by
/- Let `U` be a neighborhood of `1`. It suffices to show that there exists `s : Finset α` such
that for any `t : Finset α` disjoint from `s`, we have `∏ i ∈ t, f i ∈ U`. -/
apply cauchySeq_finset_iff_prod_vanishing.mpr
intro U hU
rcases is_nonarchimedean U hU with
⟨V, hV⟩
/- Let `s` be the set of all indices `i : α` such that `f i ∉ V`. By our assumption `hf`, this is
finite. -/
use (tendsto_def.mp hf V V.mem_nhds_one).toFinset
intro t ht
apply hV
apply Subgroup.prod_mem
intro i hi
simpa using Finset.disjoint_left.mp ht hi
