as_ideal_le_as_ideal — Mathlib

English

The order on points x,y in ProjectiveSpectrum 𝒜 is induced by the inclusion of their homogeneous ideals: x ≤ y iff x.asHomogeneousIdeal ≤ y.asHomogeneousIdeal.

Русский

Порядок точек x, y в ProjectiveSpectrum 𝒜 задаётся включением их однородных идеалов: x ≤ y тогда и только тогда, когда x.asHomogeneousIdeal ≤ y.asHomogeneousIdeal.

LaTeX

$$$x.asHomogeneousIdeal \le y.asHomogeneousIdeal \iff x \le y$$$

Lean4

@[simp]
theorem as_ideal_le_as_ideal (x y : ProjectiveSpectrum 𝒜) : x.asHomogeneousIdeal ≤ y.asHomogeneousIdeal ↔ x ≤ y :=
  Iff.rfl

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