krullDim_nonneg_iff — Mathlib

English

The Krull dimension is nonnegative if and only if the type is nonempty.

Русский

Размерность Крулл неотрицательна тогда, когда множество непустое.

LaTeX

$$$$ 0 \le \operatorname{krullDim}(\alpha) \iff \operatorname{Nonempty}(\alpha) $$$$

Lean4

theorem krullDim_nonneg_iff : 0 ≤ krullDim α ↔ Nonempty α := by
  rw [← not_iff_not, not_le, not_nonempty_iff, ← krullDim_eq_bot_iff, ← WithBot.lt_coe_bot, bot_eq_zero,
    WithBot.coe_zero]

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