krullDim_eq_iSup_height — Mathlib

English

If α ≃o β, then krullDim α = krullDim β.

Русский

Если α эквивалентно β как порядок, размерности Крулла совпадают.

LaTeX

$$\operatorname{krullDim}(\alpha) = \operatorname{krullDim}(\beta) \text{ if } \alpha \cong_o \beta$$

Lean4

/-- The Krull dimension is the supremum of the elements' heights.

If `α` is `Nonempty`, then `krullDim_eq_iSup_height_of_nonempty`, with the coercion from
`ℕ∞` to `WithBot ℕ∞` outside the supremum, can be more convenient.
-/
theorem krullDim_eq_iSup_height : krullDim α = ⨆ (a : α), ↑(height a) := by
  cases isEmpty_or_nonempty α with
  | inl h => rw [krullDim_eq_bot, ciSup_of_empty]
  | inr h => rw [krullDim_eq_iSup_height_of_nonempty, WithBot.coe_iSup (OrderTop.bddAbove _)]

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