Theorems · Definition · order theory

Order.krullDim

(α : Type u_1) → [Preorder α] → WithBot ℕ∞

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.

Defined in

Mathlib.Order.KrullDimension

Cited by

82 results in Mathlib

Foundations

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

Assumes

Preorder