isCompact_basicOpen — Mathlib

English

Each basic open set is compact in the prime spectrum topology.

Русский

Каждое базисное открытое множество компактно в топологии спектра примитивных идеалов.

LaTeX

$$$$ \\mathrm{IsCompact}(\\mathrm{basicOpen}(f) : \\{ \\cdot \\} ). $$$$

Lean4

theorem isCompact_basicOpen (f : R) : IsCompact (basicOpen f : Set (PrimeSpectrum R)) :=
  by
  rw [← localization_away_comap_range (Localization (Submonoid.powers f))]
  exact isCompact_range (map_continuous _)

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