head_add_length_le_int — Mathlib

English

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

Русский

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

LaTeX

$$$\forall p:\ LTSeries\mathbb{Z}, 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_int (p : LTSeries ℤ) : p.head + p.length ≤ p.last := by
  simpa using LTSeries.apply_add_index_le_apply_add_index_int _ _ (Fin.last _) (Fin.zero_le _)

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