height_eq_index_of_length_eq_height_last

English

Same as Height Index Theorem: height(p(i)) = i for p.length = height(p.last).

Русский

То же самое, что и Высота‑индекс: height(p(i)) = i при p.length = height(p.last).

LaTeX

$$$p.length = \operatorname{height}(p.last) \Rightarrow \forall i : Fin(p.length + 1), \operatorname{height}(p(i)) = i.$$$

Lean4

/-- In a maximally long series, i.e one as long as the height of the last element, the height of each
element is its index in the series.
-/
theorem height_eq_index_of_length_eq_height_last {p : LTSeries α} (h : p.length = height p.last)
    (i : Fin (p.length + 1)) : height (p i) = i :=
  by
  refine le_antisymm (height_le ?_) (index_le_height p i)
  intro p' hp'
  have hp'' := length_le_height_last (p := p'.smash (p.drop i) (by simpa))
  simp [← h] at hp''; clear h
  norm_cast at *
  cutsat

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