head_add_length_le_nat — Mathlib

English

In natural numbers, head plus length is at most the last element.

Русский

В ℕ сумма головы и длины не превосходит последнего элемента.

LaTeX

$$$\forall p:\ LTSeries\mathbb{N}, p.head + p.length \le p.last$$$

Lean4

/-- In ℕ, the head and tail of an `LTSeries` differ at least by the length of the series -/
theorem head_add_length_le_nat (p : LTSeries ℕ) : p.head + p.length ≤ p.last :=
  LTSeries.apply_add_index_le_apply_add_index_nat _ _ (Fin.last _) (Fin.zero_le _)

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