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)