prod_lt_prod_of_nonempty' — Mathlib

English

If s is nonempty and ∀ i ∈ s, f(i) ≤ g(i) with some i having strict inequality, then (s.map f).prod < (s.map g).prod.

Русский

Если s непусто и для всех i ∈ s выполняется f(i) ≤ g(i) с существованием элемента, где неравенство строгие, то произведение по s для f меньше произведения по s для g.

LaTeX

$$$ \left( \forall i \in s, f(i) \le g(i) \right) \rightarrow \left( \exists i \in s, f(i) < g(i) \right) \Rightarrow (s.map f).prod < (s.map g).prod $$$

Lean4

@[to_additive sum_lt_sum_of_nonempty]
theorem prod_lt_prod_of_nonempty' (hs : s ≠ ∅) (hfg : ∀ i ∈ s, f i < g i) : (s.map f).prod < (s.map g).prod :=
  by
  obtain ⟨i, hi⟩ := exists_mem_of_ne_zero hs
  exact prod_lt_prod' (fun i hi => le_of_lt (hfg i hi)) ⟨i, hi, hfg i hi⟩

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