mem_basicOpen — Mathlib

English

For any f and x in ProjectiveSpectrum 𝒜, x lies in basicOpen 𝒜 f exactly when f is not in the homogeneous ideal of x.

Русский

Для любых f и x в ProjectiveSpectrum 𝒜 точка x принадлежит basicOpen 𝒜 f тогда и только тогда, когда f не принадлежит однородному идеалу x.

LaTeX

$$$ x \in basicOpen_{\mathcal{A}}(f) \iff f \notin x.asHomogeneousIdeal $$$

Lean4

@[simp]
theorem mem_basicOpen (f : A) (x : ProjectiveSpectrum 𝒜) : x ∈ basicOpen 𝒜 f ↔ f ∉ x.asHomogeneousIdeal :=
  Iff.rfl

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