krullDim_nonpos_iff_forall_isMin — Mathlib

English

KrullDim α ≤ 0 iff every element is minimal.

Русский

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

LaTeX

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

Lean4

theorem krullDim_nonpos_iff_forall_isMin : krullDim α ≤ 0 ↔ ∀ x : α, IsMin x :=
  by
  simp only [krullDim_nonpos_iff_forall_isMax, IsMax, IsMin]
  exact forall_swap

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