English
If α is a nonempty type equipped with a preorder, then the Krull dimension of the top-extended type WithTop α equals the Krull dimension of α plus 1. Symbolically, krullDim(WithTop α) = krullDim(α) + 1, provided α ≠ ∅.
Русский
Если α непустого типа с предикатом упорядочения, то крулль-мера WithTop α равна крулль-дименсии α плюс 1. То есть krullDim(WithTop α) = krullDim(α) + 1 при α ≠ ∅.
LaTeX
$$$\\forall \\alpha\\,[\\text{Preorder }\\alpha],\\; \\text{Nonempty }\\alpha:\\; \\operatorname{krullDim}(\\WithTop\\alpha) = \\operatorname{krullDim}(\\alpha) + 1.$$$
Lean4
@[simp]
theorem krullDim_WithTop [Nonempty α] : krullDim (WithTop α) = krullDim α + 1 :=
by
rw [← height_top_eq_krullDim, krullDim_eq_iSup_height_of_nonempty, height_eq_iSup_lt_height]
norm_cast
simp_rw [WithTop.lt_top_iff_ne_top]
rw [ENat.iSup_add, iSup_subtype']
symm
apply Equiv.withTopSubtypeNe.symm.iSup_congr
simp
