English
Let G be a topological group and f: α → G. The product taken over all elements not in a finite subset s of α tends to the identity as s grows to cover α.
Русский
Пусть G — топологическая группа и f: α → G. Произведение по всем элементам, не принадлежащим конечному подмножеству s ⊂ α, стремится к единице при росте s до полного охвата α.
LaTeX
$$$$\operatorname{Tendsto}\left( s\;:\;\mathrm{Finset}\,\alpha \mapsto \prod' a : \{ x \mid x \notin s\}, f(a) \right)_{\mathrm{atTop}}\; (\mathcal{N}\,1) $$$$
Lean4
/-- The product over the complement of a finset tends to `1` when the finset grows to cover the
whole space. This does not need a multipliability assumption, as otherwise all such products are
one. -/
@[to_additive /-- The sum over the complement of a finset tends to `0` when the finset grows to
cover the whole space. This does not need a summability assumption, as otherwise all such sums are
zero. -/
]
theorem tendsto_tprod_compl_atTop_one (f : α → G) :
Tendsto (fun s : Finset α ↦ ∏' a : { x // x ∉ s }, f a) atTop (𝓝 1) := by
classical
by_cases H : Multipliable f
· intro e he
obtain ⟨s, hs⟩ := H.tprod_vanishing he
rw [Filter.mem_map, mem_atTop_sets]
exact ⟨s, fun t hts ↦ hs _ <| Set.disjoint_left.mpr fun a ha has ↦ ha (hts has)⟩
· refine tendsto_const_nhds.congr fun _ ↦ (tprod_eq_one_of_not_multipliable ?_).symm
rwa [Finset.multipliable_compl_iff]
