Spec_basicOpen — Mathlib

English

For any ring R and f in R, PrimeSpectrum.basicOpen f is an affine scheme.

Русский

Для кольца R и элемента f ∈ R, PrimeSpectrum.basicOpen f является афинной схемой.

LaTeX

$$$\text{IsAffineOpen}(\mathrm{PrimeSpectrum.basicOpen}(f))$$$

Lean4

theorem Spec_basicOpen {R : CommRingCat} (f : R) : IsAffineOpen (X := Spec R) (PrimeSpectrum.basicOpen f) :=
  basicOpen_eq_of_affine f ▸ (isAffineOpen_top (Spec <| .of R)).basicOpen _

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