Theorems · Definition · order theory

Order.coheight

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

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. 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). The definition of coheight is via the height in the dual order, in order to easily transfer theorems between height and coheight. See coheight_eq for the definition with a series ordered by < and beginning with a.

Defined in

Mathlib.Order.KrullDimension

Cited by

74 results in Mathlib

Foundations

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

Assumes

Preorder