Mathlib Map

Structures · Topology

SpectralSpace

A topological space is spectral if it is T0, compact, sober, quasi-separated, and its compact open subsets form an open basis.

Defined in
Mathlib.Topology.Spectral.Basic
Shape
One type argument

Extends5

Extended by0

Nothing extends this class yet.

Concrete types that are instances1

  • PrimeSpectrum

How is a type an instance?

Loading the hierarchy index…

Assumed by6

Ancestors6