Theorems · Theorem · sequences and series

HasProd.hasProd_of_prod_eq

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a : α}
  {g : γ → α},
  (∀ (u : Finset γ), ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b) →
    HasProd g a → HasProd f a

Defined in

Mathlib.Topology.Algebra.InfiniteSum.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommMonoidTopologicalSpace