mem_coe_basicOpen — Mathlib

English

The membership condition for the coerced basic open set agrees with the previous membership criterion.

Русский

Условие принадлежности для неявного множества basicOpen согласуется с предыдущей критериальной принадлежностью.

LaTeX

$$$ x \in (\uparrow(\mathrm{basicOpen}_{\mathcal{A}}(f)) : \mathrm{Set}(\mathrm{ProjSpec}_{\mathcal{A}})) \iff f \notin x.asHomogeneousIdeal $$$

Lean4

theorem mem_coe_basicOpen (f : A) (x : ProjectiveSpectrum 𝒜) :
    x ∈ (↑(basicOpen 𝒜 f) : Set (ProjectiveSpectrum 𝒜)) ↔ f ∉ x.asHomogeneousIdeal :=
  Iff.rfl

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