exists_le_of_sum_le — Mathlib

English

If s is nonempty and the sum over s of f is less than or equal to the sum over s of g, there exists an index i ∈ s with f(i) ≤ g(i).

Русский

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

LaTeX

$$$\text{If } s\text{ is nonempty and } \sum_{i\in s} f(i) \le \sum_{i\in s} g(i), \text{ then } \exists i \in s,\ f(i) \le g(i).$$$

Lean4

theorem exists_le_of_sum_le {s : Finset α} (hs : s.Nonempty) {f g : α → ℝ≥0∞} (Hle : ∑ i ∈ s, f i ≤ ∑ i ∈ s, g i) :
    ∃ i ∈ s, f i ≤ g i := by
  contrapose! Hle
  apply ENNReal.sum_lt_sum_of_nonempty hs Hle

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