English
The height of an element a in a preorder is the supremum over lengths of LT-series ending below or at a.
Русский
Высота элемента a в предпорядке — супремум длин LT-рядов, оканчивающихся не выше a.
LaTeX
$$$\\text{height}(a) = \\sup_{p: LTSeries(\\alpha),\\; p.last \\le a} \\; \\text{length}(p).$$$
Lean4
/-- The **height** of an element `a` in a preorder `α` is the supremum of the rightmost index of all
relation series of `α` ordered by `<` and ending below or at `a`. In other words, it is
the largest `n` such that there's a series `a₀ < a₁ < ... < aₙ = a` (or `∞` if there is
no largest `n`).
-/
noncomputable def height {α : Type*} [Preorder α] (a : α) : ℕ∞ :=
⨆ (p : LTSeries α) (_ : p.last ≤ a), p.length
