quasiSeparatedSpace_of_isAffine — Mathlib

English

If X is an affine scheme, then its underlying topological space is quasi-separated.

Русский

Если X—аффинная схема, то её топологическое пространство квазиразделимо.

LaTeX

$$$\\mathrm{IsAffine}(X) \\Rightarrow \\mathrm{QuasiSeparatedSpace}(X).$$$

Lean4

instance quasiSeparatedSpace_of_isAffine (X : Scheme) [IsAffine X] : QuasiSeparatedSpace X :=
  (quasiSeparatedSpace_congr X.isoSpec.hom.homeomorph).2 PrimeSpectrum.instQuasiSeparatedSpace

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