instSpectralSpace

Mathlib.RingTheory.Spectrum.Prime.Topology

URI: https://scilib.ai/kg/mathlib#PrimeSpectrum.instSpectralSpace

English

PrimeSpectrum(R) is a spectral space (i.e., a compact, sober, quasi-compact, etc.).

Русский

PrimeSpectrum(R) является спектральным пространством (компактным, строго непрерывным, и т.п.).

LaTeX

$$$$ \operatorname{SpectralSpace}(\operatorname{PrimeSpectrum}(R)). $$$$

Lean4

instance : SpectralSpace (PrimeSpectrum R) where

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru