Compact sets #
We define the subtype of compact sets in a topological space.
Main Definitions #
closeds αis the type of closed subsets of a topological space
compacts αis the type of compact subsets of a topological space
nonempty_compacts αis the type of non-empty compact subsets.
positive_compacts αis the type of compact subsets with non-empty interior.
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.
In an inhabited space, the type of nonempty compact subsets is also inhabited, with default element the singleton set containing the default element.
In a nonempty compact space,
set.univ is a member of
positive_compacts, the compact sets
with nonempty interior.
The image of a compact set under a continuous function.
A homeomorphism induces an equivalence on compact sets, by taking the image.
The image of a compact set under a homeomorphism can also be expressed as a preimage.
Associate to a nonempty compact subset the corresponding closed subset