prod_map_le_prod_map — Mathlib

English

If f ≤ g pointwise on a finite multiset s, then the product of f over s is ≤ the product of g over s.

Русский

Если для всех i ∈ s выполняется f(i) ≤ g(i), то произведение f по s не превосходит произведение g по s.

LaTeX

$$$ (\forall i \in s, f(i) \le g(i)) \Rightarrow (s.map f).prod \le (s.map g).prod $$$

Lean4

@[to_additive]
theorem prod_map_le_prod_map [MulLeftMono α] {s : Multiset ι} (f : ι → α) (g : ι → α) (h : ∀ i, i ∈ s → f i ≤ g i) :
    (s.map f).prod ≤ (s.map g).prod :=
  prod_le_prod_of_rel_le <| rel_map.2 <| rel_refl_of_refl_on h

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