height_le_iff — Mathlib

English

For a prime ideal p, p.height ≤ n if and only if for every prime q below p, q.height < n.

Русский

Для простого идеала p высота p ≤ n тогда и только тогда, когда для каждого простого q, расположеннго строго внутри p, height(q) < n.

LaTeX

$$$p.height \le n \iff \forall q,\; q.IsPrime \to q < p \to q.height < n.$$$

Lean4

theorem height_le_iff {p : Ideal R} {n : ℕ} [p.IsPrime] :
    p.height ≤ n ↔ ∀ q : Ideal R, q.IsPrime → q < p → q.height < n :=
  by
  rw [height_eq_primeHeight, primeHeight, Order.height_le_coe_iff, (PrimeSpectrum.equivSubtype R).forall_congr_left,
    Subtype.forall]
  congr!
  rw [height_eq_primeHeight, primeHeight]
  rfl

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