isOpen_basicOpen

Mathlib.RingTheory.Spectrum.Prime.Topology

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

English

For any r ∈ R, the basicOpen set is open in the prime spectrum topology.

Русский

Для любого r ∈ R базисное открытое множество открыто в топологии спектра примитивных идеалов.

LaTeX

$$$$ \\text{IsOpen}(\\mathrm{basicOpen}(r)). $$$$

Lean4

theorem isOpen_basicOpen {a : R} : IsOpen (basicOpen a : Set (PrimeSpectrum R)) :=
  (basicOpen a).isOpen

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

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

Разделы

Аффилиация

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