Alexandrov-discrete topological spaces #
This file defines Alexandrov-discrete spaces, aka finitely generated spaces.
A space is Alexandrov-discrete if the (arbitrary) intersection of open sets is open. As such, the intersection of all neighborhoods of a set is a neighborhood itself. Hence every set has a minimal neighborhood, which we call the exterior of the set.
Main declarations #
AlexandrovDiscrete
: Prop-valued typeclass for a topological space to be Alexandrov-discrete
Notes #
The "minimal neighborhood of a set" construction is not named in the literature. We chose the name
"exterior" with analogy to the interior. interior
and exterior
have the same properties up to
TODO #
Finite product of Alexandrov-discrete spaces is Alexandrov-discrete.
Tags #
Alexandroff, discrete, finitely generated, fg space
A topological space is Alexandrov-discrete or finitely generated if the intersection of a family of open sets is open.
The intersection of a family of open sets is an open set. Use
isOpen_sInter
in the root namespace instead.
Instances
Alias of Topology.IsInducing.alexandrovDiscrete
.