Structures · Topology
JacobsonSpace
The class of Jacobson spaces, i.e. spaces such that the set of closed points are dense in every closed subspace.
- Defined in
- Mathlib.Topology.JacobsonSpace
- Shape
- One type argument · adds closure_inter_closedPoints
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- TopCat.carrier
- PrimeSpectrum
How is a type an instance?
Loading the hierarchy index…
Assumed by15
- nonempty_inter_closedPoints
- isClosed_singleton_of_isLocallyClosed_singleton
- JacobsonSpace.of_isOpenEmbedding
- AlgebraicGeometry.LocallyOfFiniteType.jacobsonSpace
- JacobsonSpace.closure_inter_closedPoints_eq_closure
- JacobsonSpace.closure_inter_closedPoints
- Topology.IsOpenEmbedding.preimage_closedPoints
- AlgebraicGeometry.isFinite_iff_locallyOfFiniteType_of_jacobsonSpace
- subsingleton_image_closure_of_finite_of_isPreirreducible
- closure_closedPoints
- JacobsonSpace.of_isClosedEmbedding
- AlgebraicGeometry.Scheme.Hom.closePoints_subset_preimage_closedPoints
- instDiscreteTopologyOfFiniteOfJacobsonSpace
- AlgebraicGeometry.isClosed_singleton_iff_locallyOfFiniteType
- JacobsonSpace.discreteTopology
Ancestors0
No ancestors.