headI_le_sum

Mathlib.Algebra.BigOperators.Group.List.Basic

URI: https://scilib.ai/kg/mathlib#List.headI_le_sum

English

The first element of a list of natural numbers is always at most the total sum.

Русский

Первый элемент списка натуральных чисел не превосходит общую сумму.

LaTeX

$$L.headI \leq L.sum$$

Lean4

/-- This relies on `default ℕ = 0`. -/
theorem headI_le_sum (L : List ℕ) : L.headI ≤ L.sum :=
  Nat.le.intro (headI_add_tail_sum L)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru