instQuasiSeparatedSpace — Mathlib

English

PrimeSpectrum(R) is a quasi-separated space; intersections of compact open sets are compact, and basic opens form a basis of compact open sets.

Русский

Спектр Прима (PrimeSpectrum(R)) является квазисепарабельным пространством: пересечения компактых открытых множеств остаются компактными, базис образуют компактные открытые множества.

LaTeX

$$$$ \text{QuasiSeparatedSpace}(\operatorname{PrimeSpectrum}(R)). $$$$

Lean4

instance : QuasiSeparatedSpace (PrimeSpectrum R) :=
  .of_isTopologicalBasis isTopologicalBasis_basic_opens fun i j ↦ by
    simpa [← TopologicalSpace.Opens.coe_inf, ← basicOpen_mul, -basicOpen_eq_zeroLocus_compl] using isCompact_basicOpen _

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