English
Let x ∈ α and n ∈ ℕ. Then height x = n + 1 ↔ height x < ⊤ ∧ (∃ y < x with height y = n) ∧ (∀ y < x, height y ≤ n).
Русский
Пусть x ∈ α и n ∈ ℕ. Тогда height x = n + 1 тогда и только если height x < ⊤ и существует y < x с height y = n и для всех y < x выполняется height y ≤ n.
LaTeX
$$$$ \operatorname{height}(x) = n + 1 \iff \operatorname{height}(x) < \top \land (\exists y < x, \operatorname{height}(y) = n) \land (\forall y < x, \operatorname{height}(y) \le n) $$$$
Lean4
@[simp]
theorem krullDim_eq_bot_iff : krullDim α = ⊥ ↔ IsEmpty α :=
by
rw [eq_bot_iff, krullDim, iSup_le_iff]
simp only [le_bot_iff, WithBot.natCast_ne_bot, isEmpty_iff]
exact ⟨fun H x ↦ H ⟨0, fun _ ↦ x, by simp⟩, (· <| · 1)⟩
