krullDim_pos_iff — Mathlib

English

0 < krullDim α iff ∃ x y with x < y in α.

Русский

0 меньше чем размерность Крулля тогда, когда существуют элементы x < y в α.

LaTeX

$$$$ 0 < \operatorname{krullDim}(\alpha) \iff \exists x, \exists y : \alpha, x < y $$$$

Lean4

theorem krullDim_pos_iff : 0 < krullDim α ↔ ∃ x y : α, x < y :=
  by
  rw [← not_iff_not]
  push_neg
  simp_rw [← isMax_iff_forall_not_lt, ← krullDim_nonpos_iff_forall_isMax]

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