Theorems · Theorem · sequences and series

tprod_def

∀ {α : Type u_4} {β : Type u_5} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] (f : β → α) (L : SummationFilter β),
  tprod f L =
    if h : Multipliable f L then
      if L.HasSupport ∧ (Function.mulSupport f ∩ L.support).Finite then finprod (L.support.mulIndicator f)
      else if HasProd f 1 L then 1 else Exists.choose h
    else 1

Defined in

Mathlib.Topology.Algebra.InfiniteSum.Defs

Cited by

11 results in Mathlib

Foundations

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

Assumes

CommMonoidTopologicalSpace