mem_basicOpen_den — Mathlib

English

If x is a point of the projective spectrum and f is a homogeneous localization datum with denominator f.den, then x lies in the basic open set D(f.den).

Русский

Пусть x — точка проективного спектра и f задан локализацией однородных элементов с знаменателем f.den; тогда x принадлежит базовой открытке D(f.den).

LaTeX

$$$x \in \mathsf{basicOpen}_{\mathcal{A}}(f.den)$$$

Lean4

theorem mem_basicOpen_den (x : ProjectiveSpectrum.top 𝒜)
    (f : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl) :
    x ∈ ProjectiveSpectrum.basicOpen 𝒜 f.den :=
  by
  rw [ProjectiveSpectrum.mem_basicOpen]
  exact f.den_mem

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