instT1Space — Mathlib

English

The maximal spectrum is a T1 space; equivalently, every singleton {x} is closed.

Русский

Максимальный спектр является T1-пространством; эквивалентно тому, что каждый множитель {x} замкнут.

LaTeX

$$$\\operatorname{MaximalSpectrum}(R) \\text{ is a } T_1\\text{-space; equivalently } \\forall x, \\ IsClosed(\\\\{x\\\\}).$$$

Lean4

instance : T1Space <| MaximalSpectrum R :=
  ⟨fun x =>
    isClosed_induced_iff.mpr
      ⟨{toPrimeSpectrum x}, (isClosed_singleton_iff_isMaximal _).mpr x.isMaximal, by
        simpa only [← image_singleton] using preimage_image_eq { x } toPrimeSpectrum_injective⟩⟩

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