prod_map_lt_prod_map — Mathlib

English

If s is nonempty, 0 < f(i) and f(i) < g(i) for all i ∈ s, then ∏ f(i) < ∏ g(i).

Русский

Если s непусто и для всех i∈s выполняются 0 < f(i) < g(i), то произведение f(i) по s меньше произведения g(i) по s.

LaTeX

$$$$\\prod_{i \\in s} f(i) < \\prod_{i \\in s} g(i) \\quad \\text{given } s \\neq \\emptyset,\\ 0 < f(i) < g(i) \\text{ for all } i \\in s.$$$$

Lean4

theorem prod_map_lt_prod_map {ι : Type*} {s : Multiset ι} (hs : s ≠ 0) (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, ne_eq, coe_eq_zero] at *
  apply List.prod_map_lt_prod_map hs f g h0 h

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