sum_id_lt_of_lt — Mathlib

English

If m,n : ι →₀ ℕ satisfy m < n, then the total mass is strictly increasing: ∑i m(i) < ∑i n(i).

Русский

Если m,n : ι →₀ ℕ удовлетворяют m < n, то общая масса строго возрастает: \sum_i m(i) < \sum_i n(i).

LaTeX

$$$$ \forall m,n : ι \to_0 \mathbb{N},\ m < n \Rightarrow \sum_{i} m(i) < \sum_{i} n(i). $$$$

Lean4

theorem sum_id_lt_of_lt (m n : ι →₀ ℕ) (h : m < n) : (m.sum fun _ => id) < n.sum fun _ => id :=
  by
  rw [← card_toMultiset, ← card_toMultiset]
  apply Multiset.card_lt_card
  exact toMultiset_strictMono h

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