English
The coheight of a equals the supremum of the lengths of LTSeries with head at least a.
Русский
Ко‑высота a равна супремуму длин серий LTSeries с head не меньше a по порядку.
LaTeX
$$$\operatorname{coheight}(a) = \sup\{ \operatorname{length}(p) : p \in LTSeries(\alpha), a \le p.head \}. $$$
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`.
This is not the definition of `coheight`. The definition of `coheight` is via the `height` in the
dual order, in order to easily transfer theorems between `height` and `coheight`.
-/
theorem coheight_eq (a : α) : coheight a = ⨆ (p : LTSeries α) (_ : a ≤ p.head), (p.length : ℕ∞) :=
by
apply
Equiv.iSup_congr
⟨RelSeries.reverse, RelSeries.reverse, fun _ ↦ RelSeries.reverse_reverse _, fun _ ↦ RelSeries.reverse_reverse _⟩
congr! 1
