sum_lt_sum_of_nonempty — Mathlib

English

If s is nonempty and f(i) < g(i) for all i ∈ s, then ∑_{i∈s} f(i) < ∑_{i∈s} g(i).

Русский

Если s непусто и f(i) < g(i) для всех i ∈ s, то сумма ∑ f(i) меньше суммы ∑ g(i).

LaTeX

$$$s\neq \varnothing \Rightarrow \left(\forall i \in s,\ f(i) < g(i)\right) \Rightarrow \sum_{i\in s} f(i) < \sum_{i\in s} g(i)$$$

Lean4

theorem sum_lt_sum_of_nonempty {s : Finset α} (hs : s.Nonempty) {f g : α → ℝ≥0∞} (Hlt : ∀ i ∈ s, f i < g i) :
    ∑ i ∈ s, f i < ∑ i ∈ s, g i := by
  induction hs using Finset.Nonempty.cons_induction with
  | singleton => simp [Hlt _ (Finset.mem_singleton_self _)]
  | cons _ _ _ _ ih =>
    simp only [Finset.sum_cons, forall_mem_cons] at Hlt ⊢
    exact ENNReal.add_lt_add Hlt.1 (ih Hlt.2)

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