length_le_coheight — Mathlib

English

For any x and LTSeries p with head p.head, length p.length is bounded by coheight x when x ≤ p.head.

Русский

Для любого x и LTSeries p, если x ≤ p.head, то длина p≤coheight(x).

LaTeX

$$$\forall x:\alpha, \forall p : LTSeries(\alpha), x \le p.head \Rightarrow p.length \le \operatorname{coheight}(x).$$$

Lean4

theorem length_le_coheight {x : α} {p : LTSeries α} (hhead : x ≤ p.head) : p.length ≤ coheight x :=
  length_le_height (α := αᵒᵈ) (p := p.reverse) (by simpa)

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