krullDim_pos_iff_of_orderTop — Mathlib

English

For an order with a top element, krullDim α > 0 iff α is nontrivial.

Русский

Для порядка с верхним элементом: krullDim α > 0 тогда и только тогда, когда α не тривиален.

LaTeX

$$0 < \operatorname{krullDim}(\alpha) \iff \text{Nontrivial}(\alpha)$$

Lean4

theorem krullDim_pos_iff_of_orderTop [OrderTop α] : 0 < krullDim α ↔ Nontrivial α :=
  by
  rw [← not_subsingleton_iff_nontrivial, ← Order.krullDim_eq_zero_iff_of_orderTop, ← ne_eq, ← lt_or_lt_iff_ne,
    or_iff_right]
  simp [Order.krullDim_nonneg]

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