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

theorem hasProd_le_nonneg {β : Type u_1} {f g : β → ℝ} {a₁ a₂ : ℝ} (h : ∀ (i : β), f i ≤ g i) (h0 : ∀ (i : β), 0 ≤ f i) (hf : HasProd f a₁) (hg : HasProd g a₂) : a₁ ≤ a₂

HasProd is monotone for nonnegative real-valued functions. This does not follow from hasProd_le since multiplication on ℝ is not covariant.

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