coheight_eq_index_of_length_eq_head_coheight

English

If p.length = coheight(p.head), then coheight(p(i)) = i.rev.

Русский

Если p.length = coheight(p.head), тогда coheight(p(i)) = i.rev.

LaTeX

$$$p.length = \operatorname{coheight}(\mathrm{head}(p)) \Rightarrow \operatorname{coheight}(p(i)) = i^{\mathrm{rev}}.$$$

Lean4

/-- In a maximally long series, i.e one as long as the coheight of the first element, the coheight of
each element is its reverse index in the series.
-/
theorem coheight_eq_index_of_length_eq_head_coheight {p : LTSeries α} (h : p.length = coheight p.head)
    (i : Fin (p.length + 1)) : coheight (p i) = i.rev := by
  simpa using height_eq_index_of_length_eq_height_last (α := αᵒᵈ) (p := p.reverse) (by simpa) i.rev

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