English
For every x in α, the coheight of x equals the Krull dimension of the subposet {y in α | x ≤ y}.
Русский
Для каждого x в α ко-высота x равна размерности Крull подмножества {y | x ≤ y}.
LaTeX
$$$\operatorname{coheight}(x) = \operatorname{krullDim}(\{ y \in α : x \le y \})$$$
Lean4
theorem coheight_eq_krullDim_Ici {α : Type*} [Preorder α] (x : α) : (coheight x : ℕ∞) = krullDim (Set.Ici x) :=
by
rw [coheight, ← krullDim_orderDual, Order.krullDim_eq_of_orderIso (OrderIso.refl _)]
exact height_eq_krullDim_Iic _