Theorems · Theorem · order theory

Order.krullDim_eq_iSup_height_of_nonempty

∀ {α : Type u_1} [inst : Preorder α] [Nonempty α], Order.krullDim α = ↑(⨆ a, Order.height a)

The Krull dimension is the supremum of the elements' heights. This version of the lemma assumes that α is nonempty. In this case, the coercion from ℕ∞ to WithBot ℕ∞ is on the outside of the right-hand side, which is usually more convenient. If α were empty, then krullDim α = ⊥. See krullDim_eq_iSup_height for the more general version, with the coercion under the supremum.

Defined in

Mathlib.Order.KrullDimension

Cited by

4 results in Mathlib

Foundations

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

Assumes

PreorderNonempty