krullDim_pos_iff_of_orderBot — Mathlib

English

If α has a bottom element, the Krull dimension is 0 if and only if α is subsingleton.

Русский

Если в α есть нуль-элемент, размерность Крулла равна 0 тогда и только тогда, когда α subsingleton.

LaTeX

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

Lean4

theorem krullDim_pos_iff_of_orderBot [OrderBot α] : 0 < krullDim α ↔ Nontrivial α :=
  by
  rw [← not_subsingleton_iff_nontrivial, ← Order.krullDim_eq_zero_iff_of_orderBot, ← ne_eq, ← lt_or_lt_iff_ne,
    or_iff_right]
  simp [Order.krullDim_nonneg]

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