rev_index_le_coheight — Mathlib

English

For p : LTSeries α and i in Fin(p.length + 1), i.rev ≤ coheight(p(i)).

Русский

Для p : LTSeries(α) и i в Fin(p.length + 1) выполняется i.rev ≤ coheight(p(i)).

LaTeX

$$$i^{\mathrm{rev}} \le \operatorname{coheight}(p(i)).$$$

Lean4

/-- The coheight of an element in a series is larger or equal to its reverse index in the series.
-/
theorem rev_index_le_coheight (p : LTSeries α) (i : Fin (p.length + 1)) : i.rev ≤ coheight (p i) := by
  simpa using index_le_height (α := αᵒᵈ) p.reverse i.rev

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