prod_le_one' — Mathlib

English

If for all i in s we have f(i) ≤ 1, then the product over i∈s of f(i) is ≤ 1.

Русский

Если для всех i ∈ s выполняется f(i) ≤ 1, то ∏_{i∈s} f(i) ≤ 1.

LaTeX

$$$ \\forall \\iota\\, N\\, [\\text{CommMonoid } N], [\\text{PartialOrder } N], {f : \\iota \\to N} {s : \\mathrm{Finset} \\iota}, [\\text{MulLeftMono } N], ( \\forall i \\in s, f(i) \\le 1 ) \\Rightarrow \\prod_{i \\in s} f(i) \\le 1. $$$

Lean4

@[to_additive sum_nonpos]
theorem prod_le_one' [MulLeftMono N] (h : ∀ i ∈ s, f i ≤ 1) : ∏ i ∈ s, f i ≤ 1 :=
  (prod_le_prod' h).trans_eq (by rw [prod_const_one])

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