English
The Krull dimension of a preorder is the supremum of the rightmost indices of all LT-series; it is −∞ if there are no such series and +∞ if their lengths are unbounded.
Русский
Кройль размерность предрейда — супремум величин правых концов LT-рядов; если таких рядов нет, −∞; если их длины неограниченны, +∞.
LaTeX
$$$\\text{krullDim}(\\alpha) = \\sup\\{\\text{length}(p) : p \\in LTSeries(\\alpha)\\}.$$$
Lean4
/-- The **Krull dimension** of a preorder `α` is the supremum of the rightmost index of all relation
series of `α` ordered by `<`. If there is no series `a₀ < a₁ < ... < aₙ` in `α`, then its Krull
dimension is defined to be negative infinity; if the length of all series `a₀ < a₁ < ... < aₙ` is
unbounded, its Krull dimension is defined to be positive infinity.
-/
noncomputable def krullDim (α : Type*) [Preorder α] : WithBot ℕ∞ :=
⨆ (p : LTSeries α), p.length
