Theorems · Definition · sequences and series

HasProd

{α : Type u_1} →
  {β : Type u_2} →
    [CommMonoid α] →
      [TopologicalSpace α] → (β → α) → α → optParam (SummationFilter β) (SummationFilter.unconditional β) → Prop

HasProd f a L means that the (potentially infinite) product of the f b for b : β converges to a along the SummationFilter L. By default L is the unconditional one, corresponding to the limit of all finite sets towards the entire type. So we take the product over bigger and bigger finite sets. This product operation is invariant under permuting the terms (while products for more general summation filters usually are not). For the definition and many statements, α does not need to be a topological monoid, only a monoid with a topology (i.e. the multiplication is not assumed to be continuous). We only add this assumption later, for the lemmas where it is relevant. These are defined in an identical way to infinite sums (HasSum). For example, we say that the function ℕ → ℝ sending n to 1 / 2 has a product of 0, rather than saying that it does not converge as some authors would.

Defined in

Mathlib.Topology.Algebra.InfiniteSum.Defs

Cited by

157 results in Mathlib

Foundations

Depth 56 from the axioms, rests on 923 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CommMonoidTopologicalSpace