English
Let α and α′ be topological commutative monoids and e: α′ → α a surjective monoid homomorphism with e(1) = 1. For f: β → α and g: γ → α′, assume that for every a, the infinite product of f over β converges to e(a) if and only if the infinite product of g over γ converges to a. Then the infinite product of f over β equals e applied to the infinite product of g over γ:
Русский
Пусть α и α′ — топологические коммутативные мононоды, e: α′ → α — surjective гомоморфизм моноидов с e(1) = 1. Пусть f: β → α и g: γ → α′. Предположим, что для каждого a выполняется эквивалентность: бесконечный произведение f по β сходится к e(a) тогда и только тогда, когда бесконечный произведение g по γ сходится к a. Тогда бесконечный произведение f по β равно e применённому к бесконечному произведению g по γ:
LaTeX
$$$\\left( \\forall a, \\ HasProd f (e\\,a) \\iff HasProd g a \\right) \\implies \\prod' b\, f b = e\\left( \\prod' c\, g c \\right)$$$
Lean4
@[to_additive]
theorem tprod_eq_tprod_of_hasProd_iff_hasProd {α' : Type*} [CommMonoid α'] [TopologicalSpace α'] {e : α' → α}
(hes : Function.Surjective e) (h1 : e 1 = 1) {f : β → α} {g : γ → α'} (h : ∀ {a}, HasProd f (e a) ↔ HasProd g a) :
∏' b, f b = e (∏' c, g c) :=
by_cases (fun x ↦ (h.mpr x.hasProd).tprod_eq) fun hg : ¬Multipliable g ↦
by
have hf : ¬Multipliable f := mt (hes.multipliable_iff_of_hasProd_iff @h).1 hg
simp [tprod_def, hf, hg, h1]
