English
For any natural n, n ≤ krullDim α iff there exists a LTSeries of length n in α.
Русский
Для любого натурального n выполнено: n ≤ krullDim α тогда и только тогда существует LTSeries длины n в α.
LaTeX
$$\forall n\in\mathbb{N}, \ n \le \operatorname{krullDim}(\alpha) \iff \exists l:\mathrm{LTSeries}(\alpha), l.\text{length}=n$$
Lean4
theorem le_krullDim_iff {n : ℕ} : n ≤ krullDim α ↔ ∃ l : LTSeries α, l.length = n :=
by
cases isEmpty_or_nonempty α
· simp [krullDim_eq_bot]
cases finiteDimensionalOrder_or_infiniteDimensionalOrder α
· rw [krullDim_eq_length_of_finiteDimensionalOrder, Nat.cast_le]
constructor
· exact fun H ↦ ⟨(LTSeries.longestOf α).take ⟨_, Nat.lt_succ.mpr H⟩, rfl⟩
· exact fun ⟨l, hl⟩ ↦ hl ▸ l.longestOf_is_longest
· simpa [krullDim_eq_top] using SetRel.InfiniteDimensional.exists_relSeries_with_length n
