English
Let α be a preorder and a ∈ α. The coheight of a is defined as the height of a in the opposite order; equivalently, it is the supremum of the lengths of all ascending relation chains starting at a (possibly infinite).
Русский
Пусть α — это частично упорядоченное множество, и возьмём элемент a ∈ α. Ко‑высота a определяется как высота элемента a в противоположном порядке; эквивалентно, это супремум длин всех восходящих последовательностейrelation начинающихся с a (возможно бесконечный).
LaTeX
$$$\operatorname{coheight}(a) = \operatorname{height}_{\alpha^{\mathrm{op}}}(a).$$$
Lean4
/-- The **coheight** of an element `a` in a preorder `α` is the supremum of the rightmost index of all
relation series of `α` ordered by `<` and beginning with `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`).
The definition of `coheight` is via the `height` in the dual order, in order to easily transfer
theorems between `height` and `coheight`. See `coheight_eq` for the definition with a
series ordered by `<` and beginning with `a`.
-/
noncomputable def coheight {α : Type*} [Preorder α] (a : α) : ℕ∞ :=
height (α := αᵒᵈ) a
