krullDim_eq_one_iff_of_boundedOrder

English

For a bounded partial order α, krullDim α = 1 if and only if α is a simple order.

Русский

Для ограниченного частичного порядка α выполняется: krullDim α = 1 тогда и только тогда, когда α — простой порядок.

LaTeX

$$$\operatorname{krullDim}(\alpha) = 1 \iff \text{IsSimpleOrder}(\alpha)$$$

Lean4

theorem krullDim_eq_one_iff_of_boundedOrder {α : Type*} [PartialOrder α] [BoundedOrder α] :
    krullDim α = 1 ↔ IsSimpleOrder α :=
  by
  rw [le_antisymm_iff, krullDim_le_one_iff, WithBot.one_le_iff_pos, Order.krullDim_pos_iff_of_orderBot,
    isSimpleOrder_iff]
  simp only [isMin_iff_eq_bot, isMax_iff_eq_top, and_comm]

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