prod_map_le_prod_map₀ — Mathlib

English

If for all i in s, 0 ≤ f(i) and f(i) ≤ g(i), then ∏_{i∈s} f(i) ≤ ∏_{i∈s} g(i).

Русский

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

LaTeX

$$$$\\prod_{i \\in s} f(i) \\le \\prod_{i \\in s} g(i) \\quad \\text{given } 0 \\le f(i) \\le g(i) \\text{ for all } i \\in s.$$$$

Lean4

theorem prod_map_le_prod_map₀ {ι : Type*} {s : Multiset ι} (f : ι → R) (g : ι → R) (h0 : ∀ i ∈ s, 0 ≤ f i)
    (h : ∀ i ∈ s, f i ≤ g i) : (map f s).prod ≤ (map g s).prod :=
  by
  cases s using Quotient.ind
  simp only [quot_mk_to_coe, mem_coe, map_coe, prod_coe] at *
  apply List.prod_map_le_prod_map₀ f g h0 h

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