index_le_height — Mathlib

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)

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