krullDim_le_one_iff_forall_isMin — Mathlib

English

KrullDim α ≤ 1 iff for all x with x ≠ ⊤, IsMin x.

Русский

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

LaTeX

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

Lean4

theorem krullDim_le_one_iff_forall_isMin {α : Type*} [PartialOrder α] [OrderTop α] :
    krullDim α ≤ 1 ↔ ∀ x : α, x ≠ ⊤ → IsMin x := by simp [krullDim_le_one_iff, ← or_iff_not_imp_right]

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