length_le_sum_of_one_le — Mathlib

English

If every element of a list L of natural numbers is at least 1, then the length of L is at most the sum of its elements.

Русский

Если каждый элемент списка L натуральных чисел не меньше 1, то длина списка не превышает сумму его элементов.

LaTeX

$$$\text{length}(L) \le \text{sum}(L)$, assuming $L_i \ge 1$ for all i.$$

Lean4

/-- If all elements in a list are bounded below by `1`, then the length of the list is bounded
by the sum of the elements. -/
theorem length_le_sum_of_one_le (L : List ℕ) (h : ∀ i ∈ L, 1 ≤ i) : L.length ≤ L.sum := by
  induction L with
  | nil => simp
  | cons j L IH =>
    rw [sum_cons, length, add_comm]
    exact Nat.add_le_add (h _ mem_cons_self) (IH fun i hi => h i (mem_cons.2 (Or.inr hi)))

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