The contents of this file should go to Topology.Algebra.InfiniteSum, either into Basic or into another file.

theorem tprod_le_of_nonneg_of_multipliable {β : Type u_1} {f g : β → ℝ} (hfnn : 0 ≤ f) (hfg : f ≤ g) (hf : Multipliable f) (hg : Multipliable g) : ∏' (b : β), f b ≤ ∏' (b : β), g b