exists_le_of_prod_le' — Mathlib

English

If s is nonempty and the product of f over s is ≤ the product of g over s, then there exists i ∈ s with f(i) ≤ g(i).

Русский

Если s непусто и произведение f по s не превосходит произведение g по s, тогда существует i ∈ s такое, что f(i) ≤ g(i).

LaTeX

$$$s \neq \varnothing \implies \left( \prod_{i \in s} f(i) \le \prod_{i \in s} g(i) \Rightarrow \exists i \in s,\ f(i) \le g(i) \right)$$$

Lean4

@[to_additive exists_le_of_sum_le]
theorem exists_le_of_prod_le' (hs : s.Nonempty) (Hle : ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i) : ∃ i ∈ s, f i ≤ g i :=
  by
  contrapose! Hle with Hlt
  exact prod_lt_prod_of_nonempty' hs Hlt

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