English
For every x in α, the height of x equals the Krull dimension of the subposet consisting of all elements ≤ x.
Русский
Для каждого x в α высота x равна размерности Крull подчасти, состоящей из элементов ≤ x.
LaTeX
$$$\\operatorname{height}(x) = \\operatorname{krullDim}(\\{ y \in \\alpha : y \\le x \\})$$$
Lean4
theorem height_eq_krullDim_Iic (x : α) : (height x : ℕ∞) = krullDim (Set.Iic x) :=
by
rw [← height_top_eq_krullDim, height, height, WithBot.coe_inj]
apply le_antisymm
· apply iSup_le; intro p; apply iSup_le; intro hp
let q :=
LTSeries.mk p.length (fun i ↦ (⟨p.toFun i, le_trans (p.monotone (Fin.le_last _)) hp⟩ : Set.Iic x))
(fun _ _ h ↦ p.strictMono h)
simp only [le_top, iSup_pos, ge_iff_le]
exact le_iSup (fun p ↦ (p.length : ℕ∞)) q
· apply iSup_le; intro p; apply iSup_le; intro _
have mono : StrictMono (fun (y : Set.Iic x) ↦ y.1) := fun _ _ h ↦ h
rw [← LTSeries.map_length p (fun x ↦ x.1) mono, ]
refine le_iSup₂ (f := fun p hp ↦ (p.length : ℕ∞)) (p.map (fun x ↦ x.1) mono) ?_
exact (p.toFun (Fin.last p.length)).2
