exists_lt_of_prod_lt' — Mathlib

English

If the product over s of f is strictly less than the product over s of g, then there exists an index i ∈ s such that f(i) < g(i) (assuming left-monotone multiplication).

Русский

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

LaTeX

$$$\left( \prod_{i \in s} f(i) < \prod_{i \in s} g(i) \right) \implies \left( \exists i \in s,\ f(i) < g(i) \right)$$$

Lean4

@[to_additive exists_lt_of_sum_lt]
theorem exists_lt_of_prod_lt' [MulLeftMono M] (Hlt : ∏ i ∈ s, f i < ∏ i ∈ s, g i) : ∃ i ∈ s, f i < g i :=
  by
  contrapose! Hlt with Hle
  exact prod_le_prod' Hle

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