English
A Cauchy sequence for the set-based product is equivalent to a tail-vanishing condition for tprod over sets.
Русский
Критерий Коши для tprod эквивалентен условию исчезновения хвоста произведений по множествам.
LaTeX
$$Same as above in tprod form: contains tail-vanishing equivalence with tprod.$$
Lean4
@[to_additive]
theorem cauchySeq_finset_iff_tprod_vanishing :
(CauchySeq fun s : Finset β ↦ ∏ b ∈ s, f b) ↔
∀ e ∈ 𝓝 (1 : α), ∃ s : Finset β, ∀ t : Set β, Disjoint t s → (∏' b : t, f b) ∈ e :=
by
simp_rw [cauchySeq_finset_iff_prod_vanishing, Set.disjoint_left, disjoint_left]
refine ⟨fun vanish e he ↦ ?_, fun vanish e he ↦ ?_⟩
· obtain ⟨o, ho, o_closed, oe⟩ := exists_mem_nhds_isClosed_subset he
obtain ⟨s, hs⟩ := vanish o ho
refine ⟨s, fun t hts ↦ oe ?_⟩
by_cases ht : Multipliable fun a : t ↦ f a
·
classical
refine o_closed.mem_of_tendsto ht.hasProd (Eventually.of_forall fun t' ↦ ?_)
rw [← prod_subtype_map_embedding fun _ _ ↦ by rfl]
apply hs
simp_rw [Finset.mem_map]
rintro _ ⟨b, -, rfl⟩
exact hts b.prop
· exact tprod_eq_one_of_not_multipliable ht ▸ mem_of_mem_nhds ho
· obtain ⟨s, hs⟩ := vanish _ he
exact ⟨s, fun t hts ↦ (t.tprod_subtype f).symm ▸ hs _ hts⟩
