English
Let f: β → α and g: γ → α be functions into a topological commutative monoid α. If for every a, HasProd f a holds if and only if HasProd g a holds, then the infinite product over β of f equals the infinite product over γ of g.
Русский
Пусть f: β → α и g: γ → α — отображения в топологический коммутативный моноид α. Если для каждого a выполняется HasProd f a ⇔ HasProd g a, то бесконечный произведение по β от f равно бесконечному произведению по γ от g.
LaTeX
$$$\\forall f:\\beta\\to\\alpha\\,\\forall g:\\gamma\\to\\alpha,\\Big( \\forall a,\\ HasProd f a \\iff HasProd g a \\Big) \\Rightarrow \\prod' b\\, f b = \\prod' c\\, g c$$$
Lean4
@[to_additive]
theorem tprod_eq_tprod_of_hasProd_iff_hasProd {f : β → α} {g : γ → α} (h : ∀ {a}, HasProd f a ↔ HasProd g a) :
∏' b, f b = ∏' c, g c :=
surjective_id.tprod_eq_tprod_of_hasProd_iff_hasProd rfl @h
