prod_lt_prod' — Mathlib

English

If f ≤ g pointwise on s and there exists i ∈ s with f(i) < g(i), then (s.map f).prod < (s.map g).prod.

Русский

Если f(i) ≤ g(i) для всех i ∈ s и существует i ∈ s such that 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]
theorem prod_lt_prod' (hle : ∀ i ∈ s, f i ≤ g i) (hlt : ∃ i ∈ s, f i < g i) : (s.map f).prod < (s.map g).prod :=
  by
  obtain ⟨l⟩ := s
  simp only [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.prod_coe]
  exact List.prod_lt_prod' f g hle hlt

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