krullDim_orderDual — Mathlib

English

Krull dimension is unchanged by dualization: krullDim (OrderDual α) = krullDim α.

Русский

Размерность Крулла неизменна при двойственном порядке.

LaTeX

$$\operatorname{krullDim}(\alpha^{\mathrm{dual}}) = \operatorname{krullDim}(\alpha)$$

Lean4

@[simp]
theorem krullDim_orderDual : krullDim αᵒᵈ = krullDim α :=
  le_antisymm (iSup_le fun i ↦ le_sSup ⟨i.reverse, rfl⟩) <| iSup_le fun i ↦ le_sSup ⟨i.reverse, rfl⟩

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