Closed sets #
We define a few types of closed sets in a topological space.
Main Definitions #
For a topological space α
,
TopologicalSpace.Closeds α
: The type of closed sets.TopologicalSpace.Clopens α
: The type of clopen sets.
Closed sets #
The type of closed subsets of a topological space.
Instances For
See Note [custom simps projection].
Instances For
The closure of a set, as an element of TopologicalSpace.Closeds
.
Instances For
The galois coinsertion between sets and opens.
Instances For
The type of closed sets is inhabited, with default element the empty set.
The term of TopologicalSpace.Closeds α
corresponding to a singleton.
Instances For
The complement of a closed set as an open set.
Instances For
The complement of an open set as a closed set.
Instances For
TopologicalSpace.Closeds.compl
as an OrderIso
to the order dual of
TopologicalSpace.Opens α
.
Instances For
TopologicalSpace.Opens.compl
as an OrderIso
to the order dual of
TopologicalSpace.Closeds α
.
Instances For
in a T1Space
, atoms of TopologicalSpace.Closeds α
are precisely the
TopologicalSpace.Closeds.singleton
s.
TODO: use minimal_nonempty_closed_eq_singleton
to show that an atom in TopologicalSpace.Closeds
in a T₀ space is a singleton.
in a T1Space
, coatoms of TopologicalSpace.Opens α
are precisely complements of singletons:
(TopologicalSpace.Closeds.singleton x).compl
.
Clopen sets #
The type of clopen sets of a topological space.
Instances For
See Note [custom simps projection].
Instances For
Reinterpret a clopen as an open.