krullDim_lt_coe_iff — Mathlib

English

If f is strictly monotone, then Krull dimension does not decrease along f.

Русский

Если f строго монотонна, то размерность Крулла не убывает при применении f.

LaTeX

$$\operatorname{krullDim}(\alpha) \le \operatorname{krullDim}(\beta) \\text{ for } f: \alpha \to \beta \text{ StrictMono}$$

Lean4

theorem krullDim_lt_coe_iff {n : ℕ} : krullDim α < n ↔ ∀ l : LTSeries α, l.length < n :=
  by
  rw [krullDim, ← WithBot.coe_natCast]
  rcases n with - | n
  · rw [ENat.coe_zero, ← bot_eq_zero, WithBot.lt_coe_bot]
    simp
  · simp [WithBot.lt_add_one_iff, WithBot.coe_natCast, Nat.lt_succ]

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