krullDim_eq_zero_iff_of_orderBot — Mathlib

English

For a partial order with an order bottom element, krullDim α = 0 exactly when α is subsingleton.

Русский

Для частичного порядка с наименьшим элементом: krullDim α = 0 тогда и только тогда, когда α subsingleton.

LaTeX

$$\operatorname{krullDim}(\alpha) = 0 \iff \text{Subsingleton}(\alpha)$$

Lean4

theorem krullDim_eq_zero_iff_of_orderBot [OrderBot α] : krullDim α = 0 ↔ Subsingleton α :=
  ⟨fun H ↦ subsingleton_of_forall_eq ⊥ fun _ ↦ le_bot_iff.mp (krullDim_nonpos_iff_forall_isMax.mp H.le ⊥ bot_le),
    fun _ ↦ Order.krullDim_eq_zero⟩

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