krullDim_nonpos_iff_forall_isMax — Mathlib

English

KrullDim α ≤ 0 if and only if every element is maximal.

Русский

Размерность Крулля не превышает 0 тогда, когда каждый элемент является максимальным.

LaTeX

$$$$ \operatorname{krullDim}(\alpha) \le 0 \iff \forall x : \alpha, \operatorname{IsMax}(x) $$$$

Lean4

theorem krullDim_nonpos_iff_forall_isMax : krullDim α ≤ 0 ↔ ∀ x : α, IsMax x :=
  by
  simp only [krullDim, iSup_le_iff, isMax_iff_forall_not_lt]
  refine ⟨fun H x y h ↦ (H ⟨1, ![x, y], fun i ↦ by obtain rfl := Subsingleton.elim i 0; simpa⟩).not_gt (by simp), ?_⟩
  · rintro H ⟨_ | n, l, h⟩
    · simp
    · cases H (l 0) (l 1) (h 0)

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