prod_map_le_pow_card — Mathlib

English

For a function f and a multiset t, the product ∏ f over t is bounded by r^{card(t)} provided 0 ≤ f ≤ r pointwise.

Русский

Произведение функции по мультиmножесту ограничено сверху r^{card(t)}, если 0 ≤ f(x) ≤ r для всех x∈t.

LaTeX

$$$$\\prod_{x \\in t} f(x) \\le r^{|t|} \\quad \\text{given } 0 \\le f(x) \\le r \\text{ for all } x \\in t.$$$$

Lean4

theorem prod_map_le_pow_card {F L : Type*} [FunLike F L R] {f : F} {r : R} {t : Multiset L} (hf0 : ∀ x ∈ t, 0 ≤ f x)
    (hf : ∀ x ∈ t, f x ≤ r) : (map f t).prod ≤ r ^ card t :=
  by
  induction t using Quotient.inductionOn
  simp_all [List.prod_map_le_pow_length₀]

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