prod_le_one — Mathlib

English

If every i in s satisfies 0 < f(i), then 0 < ∏ f(i).

Русский

Если для каждого i в s выполняется 0 < f(i), то произведение положительно.

LaTeX

$$$$0 < \\prod_{i ∈ s} f(i) \\quad \\text{given } \\forall i ∈ s, 0 < f(i).$$$$

Lean4

/-- If each `f i`, `i ∈ s` belongs to `[0, 1]`, then their product is less than or equal to one.
See also `Finset.prod_le_one'` for the case of an ordered commutative multiplicative monoid. -/
theorem prod_le_one (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ 1) : ∏ i ∈ s, f i ≤ 1 :=
  by
  convert ← prod_le_prod h0 h1
  exact Finset.prod_const_one

Похожие утверждения