exists_lt_of_prod_lt' — Mathlib

English

If a product decreases strictly, there must be a place i in the list where f(i) < g(i). More precisely, if (l.map f).prod < (l.map g).prod, then there exists i ∈ l with f(i) < g(i).

Русский

Если произведение уменьшается строго, существует элемент списка i, для которого f(i) < g(i). Точнее, если (l.map f).prod < (l.map g).prod, то найдется i ∈ l такое, что f(i) < g(i).

LaTeX

$$$(l.map f).prod < (l.map g).prod \\Rightarrow \\exists i\\in l,\\ f(i) < g(i).$$

Lean4

@[to_additive exists_lt_of_sum_lt]
theorem exists_lt_of_prod_lt' [LinearOrder M] [MulRightMono M] [MulLeftMono M] {l : List ι} (f g : ι → M)
    (h : (l.map f).prod < (l.map g).prod) : ∃ i ∈ l, f i < g i :=
  by
  contrapose! h
  exact prod_le_prod' h

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