English
KrullDim α ≤ 1 iff every element is either minimal or maximal.
Русский
Размерность Крулля ≤ 1 тогда и только тогда каждый элемент либо минимален, либо максимален.
LaTeX
$$$$ \operatorname{krullDim}(\alpha) \le 1 \iff \forall x : \alpha, \operatorname{IsMin}(x) \lor \operatorname{IsMax}(x) $$$$
Lean4
theorem krullDim_le_one_iff : krullDim α ≤ 1 ↔ ∀ x : α, IsMin x ∨ IsMax x :=
by
rw [← not_iff_not]
simp_rw [isMax_iff_forall_not_lt, isMin_iff_forall_not_lt, krullDim, iSup_le_iff]
push_neg
constructor
· rintro ⟨⟨_ | _ | n, l, hl⟩, hl'⟩
iterate 2 · cases hl'.not_ge (by simp)
exact ⟨l 1, ⟨l 0, hl 0⟩, l 2, hl 1⟩
· rintro ⟨x, ⟨y, hxy⟩, z, hzx⟩
exact ⟨⟨2, ![y, x, z], fun i ↦ by fin_cases i <;> simpa⟩, by simp⟩
