Theorems · Definition · order theory

Order.height

{α : Type u_1} → [Preorder α] → α → ℕ∞

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).

Defined in

Mathlib.Order.KrullDimension

Cited by

67 results in Mathlib

Foundations

Depth 32 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Preorder