spec_le_iff — Mathlib

English

In the prime spectrum Spec R, the preorder relation p ≤ q corresponds to reverse inclusion of the corresponding prime ideals: q.asIdeal ⊆ p.asIdeal.

Русский

В спектре примар Spec R отношение p ≤ q эквивалентно обратному включению соответствующих идеалов: q.asIdeal ⊆ p.asIdeal.

LaTeX

$$$p \le q \iff q.asIdeal \subseteq p.asIdeal$ in Spec R$$

Lean4

theorem spec_le_iff (R : CommRingCat) (p q : Spec R) : p ≤ q ↔ q.asIdeal ≤ p.asIdeal := by
  aesop (add simp PrimeSpectrum.le_iff_specializes)

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