krullDim_le_one_iff_forall_isMax — Mathlib

English

KrullDim α ≤ 1 iff for all x with x ≠ ⊥, IsMax x.

Русский

KrullDim α ≤ 1 эквивалентно тому, что для всех x ≠ ⊥, x является максимальным.

LaTeX

$$$$ \operatorname{krullDim}(\alpha) \le 1 \iff \forall x : \alpha, x \neq \bot \to \operatorname{IsMax}(x) $$$$

Lean4

theorem krullDim_le_one_iff_forall_isMax {α : Type*} [PartialOrder α] [OrderBot α] :
    krullDim α ≤ 1 ↔ ∀ x : α, x ≠ ⊥ → IsMax x := by simp [krullDim_le_one_iff, ← or_iff_not_imp_left]

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