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)