Documentation

Mathlib.Topology.Spectral.Prespectral

Prespectral spaces #

In this file, we define prespectral spaces as spaces whose lattice of compact opens forms a basis.

A space is prespectral if the lattice of compact opens forms a basis.

Instances
    theorem PrespectralSpace.of_isTopologicalBasis {X : Type u_1} [TopologicalSpace X] {B : Set (Set X)} (basis : TopologicalSpace.IsTopologicalBasis B) (isCompact_basis : UB, IsCompact U) :

    A space is prespectral if it has a basis consisting of compact opens.

    theorem PrespectralSpace.of_isTopologicalBasis' {X : Type u_1} [TopologicalSpace X] {ι : Type u_3} {b : ιSet X} (basis : TopologicalSpace.IsTopologicalBasis (Set.range b)) (isCompact_basis : ∀ (i : ι), IsCompact (b i)) :

    A space is prespectral if it has a basis consisting of compact opens. This is the variant with an indexed basis instead.

    instance PrespectralSpace.sigma {ι : Type u_3} (X : ιType u_4) [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), PrespectralSpace (X i)] :
    PrespectralSpace ((i : ι) × X i)

    In a prespectral space, the lattice of opens is determined by its lattice of compact opens.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem IsOpenMap.exists_opens_image_eq_of_prespectralSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [PrespectralSpace X] {f : XY} (hfc : Continuous f) (h : IsOpenMap f) {U : Set Y} (hs : U Set.range f) (hU : IsOpen U) (hc : IsCompact U) :

      If X has a basis of compact opens and f : X → S is open, every compact open of S is the image of a compact open of X.