instPartialOrder — Mathlib

English

There is a natural partial order on ProjectiveSpectrum 𝒜 defined by inclusion of the corresponding homogeneous ideals.

Русский

Существет естественный частичный порядок на ProjectiveSpectrum 𝒜, заданный включением соответствующих однородных идеалов.

LaTeX

$$$P \le Q \;\Leftrightarrow\; P.asHomogeneousIdeal \subseteq Q.asHomogeneousIdeal$$$

Lean4

instance : PartialOrder (ProjectiveSpectrum 𝒜) :=
  PartialOrder.lift asHomogeneousIdeal fun ⟨_, _, _⟩ ⟨_, _, _⟩ => by simp only [mk.injEq, imp_self]

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