instPrespectralSpace — Mathlib

English

PrimeSpectrum(R) is a prespectral space: the basic opens form a basis of compact open sets with appropriate properties.

Русский

PrimeSpectrum(R) является prespectral пространством: базисом открытых компактных множеств служат базовые открытые множества.

LaTeX

$$$$ \mathrm{PrespectralSpace}(\operatorname{PrimeSpectrum}(R)). $$$$

Lean4

instance : PrespectralSpace (PrimeSpectrum R) :=
  .of_isTopologicalBasis' isTopologicalBasis_basic_opens isCompact_basicOpen

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