finiteDimensionalOrder_iff_krullDim_ne_bot_and_top

English

For any α, α is finite-dimensional iff the Krull dimension is strictly between bottom and top, i.e., krullDim α ≠ ⊥ and krullDim α ≠ ⊤.

Русский

Для любого α верно: α имеет конечную размерность тогда и только тогда, когда размерность Крull не равна нижнему и не равна верхнему пределу.

LaTeX

$$$\operatorname{FiniteDimensionalOrder}(\alpha) \iff (\operatorname{krullDim}(\alpha) \neq ⊥) \land (\operatorname{krullDim}(\alpha) \neq ⊤)$$$

Lean4

theorem finiteDimensionalOrder_iff_krullDim_ne_bot_and_top :
    FiniteDimensionalOrder α ↔ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤ :=
  by
  by_cases h : Nonempty α
  · simp [← not_infiniteDimensionalOrder_iff, ← krullDim_eq_top_iff]
  · constructor
    · exact (fun h1 ↦ False.elim (h (LTSeries.nonempty_of_finiteDimensionalOrder α)))
    · exact (fun h1 ↦ False.elim (h1.1 (krullDim_eq_bot_iff.mpr (not_nonempty_iff.mp h))))

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