Documentation

Mathlib.Topology.JacobsonSpace

Jacobson spaces #

Main results #

References #

def closedPoints (X : Type u_1) [TopologicalSpace X] :
Set X

The set of closed points.

Equations
Instances For

    The class of jacobson spaces, i.e. spaces such that the set of closed points are dense in every closed subspace.

    Stacks Tag 005U

    Instances
      @[instance 100]
      theorem jacobsonSpace_iff_of_iSup_eq_top {X : Type u_2} [TopologicalSpace X] {ι : Type u_1} {U : ιTopologicalSpace.Opens X} (hU : iSup U = ) :
      JacobsonSpace X ∀ (i : ι), JacobsonSpace (U i)