Theorems · Theorem · sequences and series

tendsto_tprod_compl_atTop_one

∀ {α : Type u_1} {G : Type u_4} [inst : TopologicalSpace G] [inst_1 : CommGroup G] [IsTopologicalGroup G] (f : α → G),
  Filter.Tendsto (fun s => ∏' (a : { x // x ∉ s }), f ↑a) Filter.atTop (nhds 1)

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.

Defined in

Mathlib.Topology.Algebra.InfiniteSum.Group

Cited by

0 results in Mathlib

Foundations

Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceCommGroupIsTopologicalGroup