krullDim_withBot — Mathlib

English

If α is a nonempty preorder, then the Krull dimension of the bottom-extended type WithBot α equals the Krull dimension of α plus 1. In symbols, krullDim(WithBot α) = krullDim α + 1, for nonempty α.

Русский

Если α непустого порядка, то крullDim WithBot α равна крullDim α плюс 1.

LaTeX

$$$\\forall \\alpha\\,[\\text{Preorder }\\alpha],\\; \\operatorname{Nonempty }\\alpha:\\; \\operatorname{krullDim}(\\WithBot\\alpha) = \\operatorname{krullDim}(\\alpha) + 1.$$$

Lean4

@[simp]
theorem krullDim_withBot [Nonempty α] : krullDim (WithBot α) = krullDim α + 1 :=
  by
  conv_lhs => rw [← krullDim_orderDual]
  conv_rhs => rw [← krullDim_orderDual]
  exact krullDim_WithTop (α := αᵒᵈ)

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