prod_le_pow_card — Mathlib

English

If all f(i) ≤ n for i in s, then ∏_{i∈s} f(i) ≤ n^{|s|}. In particular, product is bounded by n raised to the cardinality of s.

Русский

Если все f(i) ≤ n для i∈s, то ∏_{i∈s} f(i) ≤ n^{|s|}.

LaTeX

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

Lean4

@[to_additive sum_le_card_nsmul]
theorem prod_le_pow_card [MulLeftMono N] (s : Finset ι) (f : ι → N) (n : N) (h : ∀ x ∈ s, f x ≤ n) :
    s.prod f ≤ n ^ #s := by
  refine (Multiset.prod_le_pow_card (s.val.map f) n ?_).trans ?_
  · simpa using h
  · simp

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