height_top_eq_krullDim — Mathlib

English

If α has a top element, then the height of the top equals the Krull dimension of α.

Русский

Если у множества α есть верхняя грань, то высота вершины верхнего элемента равна размерности Крull α.

LaTeX

$$$\operatorname{height}(\top) = \operatorname{krullDim}(\alpha)$$$

Lean4

@[simp] -- not as useful as a simp lemma as it looks, due to the coe on the left

theorem height_top_eq_krullDim [OrderTop α] : height (⊤ : α) = krullDim α :=
  by
  rw [krullDim_eq_iSup_length]
  simp only [WithBot.coe_inj]
  apply le_antisymm
  · exact height_le fun p _ ↦ le_iSup_of_le p le_rfl
  · exact iSup_le fun _ => length_le_height le_top

Похожие утверждения