topological_space.opens

The type of open subsets of a topological space.

topological_space.closeds

The type of closed subsets of a topological space.

topological_space.nonempty_compacts

The type of non-empty compact subsets of a topological space. The non-emptiness will be useful in metric spaces, as we will be able to put a distance (and not merely an edistance) on this space.

topological_space.nonempty_compacts.to_closeds

Associate to a nonempty compact subset the corresponding closed subset