English
If a LTSeries p satisfies p.length = height(p.last), then height(p(i)) = i for all i in its index range.
Русский
Если для LTSeries p выполнено p.length = height(p.last), то height(p(i)) = i для всех допустимых i.
LaTeX
$$$p.length = \operatorname{height}(p.last) \Rightarrow \forall i : Fin(p.length + 1), \operatorname{height}(p(i)) = i.$$$
Lean4
/-- The height of an element in a series is larger or equal to its index in the series.
-/
theorem index_le_height (p : LTSeries α) (i : Fin (p.length + 1)) : i ≤ height (p i) :=
length_le_height_last (p := p.take i)