quasiSober — Mathlib

English

PrimeSpectrum R is a quasi-sober space.

Русский

Спектр примар R является квазисдержанным пространством.

LaTeX

$$$\\text{QuasiSober}(\\operatorname{PrimeSpectrum}(R))$$$

Lean4

instance quasiSober : QuasiSober (PrimeSpectrum R) :=
  ⟨fun {S} h₁ h₂ =>
    ⟨⟨_, isIrreducible_iff_vanishingIdeal_isPrime.1 h₁⟩, by
      rw [IsGenericPoint, closure_singleton, zeroLocus_vanishingIdeal_eq_closure, h₂.closure_eq]⟩⟩

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