toPrimeSpectrum_continuous

Mathlib.RingTheory.Spectrum.Maximal.Topology

URI: https://scilib.ai/kg/mathlib#MaximalSpectrum.toPrimeSpectrum_continuous

English

The map from the maximal spectrum to the prime spectrum is continuous.

Русский

Отображение из максимального спектра в простейший спектр непрерывно.

LaTeX

$$$\\operatorname{Continuous}(\\\\operatorname{toPrimeSpectrum})$$$

Lean4

theorem toPrimeSpectrum_continuous : Continuous <| @toPrimeSpectrum R _ :=
  continuous_induced_dom

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

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

Разделы

Аффилиация

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