product/sum of positive reals is positive

Stream: new members

[Horatiu Cheval]

Does such a lemma exist? And the same question for sums. Or is it a wrong approach for working with partial sums?

import data.real.basic

open_locale big_operators

example (x : ℕ → ℝ) (n : ℕ) (h : ∀ i, 0 ≤ x i) : 0 ≤ ∏ i : finset.range n, x i :=
sorry

[Eric Rodriguez]

docs#finset.prod_nonneg

[Eric Rodriguez]

(gptf found that for me, but the name seems pretty guessable)

[Eric Rodriguez]

finset.prod_nonneg (λ i _, h i)

[Horatiu Cheval]

Thanks!