Compact sets #
We define a few types of compact sets in a topological space.
Main Definitions #
For a topological space α
,
TopologicalSpace.Compacts α
: The type of compact sets.TopologicalSpace.NonemptyCompacts α
: The type of non-empty compact sets.TopologicalSpace.PositiveCompacts α
: The type of compact sets with non-empty interior.TopologicalSpace.CompactOpens α
: The type of compact open sets. This is a central object in the study of spectral spaces.
Compact sets #
The type of compact sets of a topological space.
Instances For
See Note [custom simps projection].
Instances For
The type of compact sets is inhabited, with default element the empty set.
The image of a compact set under a continuous function.
Instances For
A homeomorphism induces an equivalence on compact sets, by taking the image.
Instances For
The image of a compact set under a homeomorphism can also be expressed as a preimage.
The product of two TopologicalSpace.Compacts
, as a TopologicalSpace.Compacts
in the product
space.
Instances For
Nonempty compact sets #
- carrier : Set α
- isCompact' : IsCompact s.carrier
- nonempty' : Set.Nonempty s.carrier
The type of nonempty compact sets of a topological space.
Instances For
See Note [custom simps projection].
Instances For
Reinterpret a nonempty compact as a closed set.
Instances For
In an inhabited space, the type of nonempty compact subsets is also inhabited, with default element the singleton set containing the default element.
The product of two TopologicalSpace.NonemptyCompacts
, as a TopologicalSpace.NonemptyCompacts
in the product space.
Instances For
Positive compact sets #
- carrier : Set α
- isCompact' : IsCompact s.carrier
- interior_nonempty' : Set.Nonempty (interior s.carrier)
The type of compact sets with nonempty interior of a topological space.
See also TopologicalSpace.Compacts
and TopologicalSpace.NonemptyCompacts
.
Instances For
See Note [custom simps projection].
Instances For
Reinterpret a positive compact as a nonempty compact.
Instances For
The image of a positive compact set under a continuous open map.
Instances For
In a nonempty locally compact space, there exists a compact set with nonempty interior.
The product of two TopologicalSpace.PositiveCompacts
, as a TopologicalSpace.PositiveCompacts
in the product space.
Instances For
Compact open sets #
The type of compact open sets of a topological space. This is useful in non Hausdorff contexts, in particular spectral spaces.
Instances For
See Note [custom simps projection].
Instances For
Reinterpret a compact open as an open.
Instances For
Reinterpret a compact open as a clopen.
Instances For
The image of a compact open under a continuous open map.
Instances For
The product of two TopologicalSpace.CompactOpens
, as a TopologicalSpace.CompactOpens
in the
product space.