Compact sets and compact spaces #
Main definitions #
We define the following properties for sets in a topological space:
IsCompact
: a set such that each open cover has a finite subcover. This is defined in mathlib using filters. The main property of a compact set isIsCompact.elim_finite_subcover
.CompactSpace
: typeclass stating that the whole space is a compact set.NoncompactSpace
: a space that is not a compact space.
Main results #
isCompact_univ_pi
: Tychonov's theorem - an arbitrary product of compact sets is compact.
A set s
is compact if for every nontrivial filter f
that contains s
,
there exists a ∈ s
such that every set of f
meets every neighborhood of a
.
Equations
- IsCompact s = ∀ ⦃f : Filter α⦄ [inst_1 : Filter.NeBot f], f ≤ Filter.principal s → ∃ a, a ∈ s ∧ ClusterPt a f
Instances For
The complement to a compact set belongs to a filter f
if each a ∈ s
has a neighborhood t
within s
such that tᶜ
belongs to f
.
If p : Set α → Prop
is stable under restriction and union, and each point x
of a compact set s
has a neighborhood t
within s
such that p t
, then p s
holds.
The intersection of a compact set and a closed set is a compact set.
The intersection of a closed set and a compact set is a compact set.
The set difference of a compact set and an open set is a compact set.
A closed subset of a compact set is a compact set.
Alias of the forward direction of isCompact_iff_ultrafilter_le_nhds
.
For every open directed cover of a compact set, there exists a single element of the cover which itself includes the set.
The neighborhood filter of a compact set is disjoint with a filter l
if and only if the
neighborhood filter of each point of this set is disjoint with l
.
A filter l
is disjoint with the neighborhood filter of a compact set if and only if it is
disjoint with the neighborhood filter of each point of this set.
For every directed family of closed sets whose intersection avoids a compact set, there exists a single element of the family which itself avoids this compact set.
For every family of closed sets whose intersection avoids a compact set, there exists a finite subfamily whose intersection avoids this compact set.
If s
is a compact set in a topological space α
and f : ι → Set α
is a locally finite
family of sets, then f i ∩ s
is nonempty only for a finitely many i
.
To show that a compact set intersects the intersection of a family of closed sets, it is sufficient to show that it intersects every finite subfamily.
Cantor's intersection theorem: the intersection of a directed family of nonempty compact closed sets is nonempty.
Cantor's intersection theorem for sequences indexed by ℕ
:
the intersection of a decreasing sequence of nonempty compact closed sets is nonempty.
For every open cover of a compact set, there exists a finite subcover.
A set s
is compact if for every family of closed sets whose intersection avoids s
,
there exists a finite subfamily whose intersection avoids s
.
A set s
is compact if and only if
for every family of closed sets whose intersection avoids s
,
there exists a finite subfamily whose intersection avoids s
.
If s : Set (α × β)
belongs to 𝓝 x ×ˢ l
for all x
from a compact set K
,
then it belongs to (𝓝ˢ K) ×ˢ l
,
i.e., there exist an open U ⊇ K
and t ∈ l
such that U ×ˢ t ⊆ s
.
If s : Set (α × β)
belongs to l ×ˢ 𝓝 y
for all y
from a compact set K
,
then it belongs to l ×ˢ (𝓝ˢ K)
,
i.e., there exist t ∈ l
and an open U ⊇ K
such that t ×ˢ U ⊆ s
.
To show that ∀ y ∈ K, P x y
holds for x
close enough to x₀
when K
is compact,
it is sufficient to show that for all y₀ ∈ K
there P x y
holds for (x, y)
close enough
to (x₀, y₀)
.
Provided for backwards compatibility,
see IsCompact.mem_prod_nhdsSet_of_forall
for a stronger statement.
If V : ι → Set α
is a decreasing family of closed compact sets then any neighborhood of
⋂ i, V i
contains some V i
. We assume each V i
is compact and closed because α
is
not assumed to be Hausdorff. See exists_subset_nhd_of_compact
for version assuming this.
If α
has a basis consisting of compact opens, then an open set in α
is compact open iff
it is a finite union of some elements in the basis
Filter.cocompact
is the filter generated by complements to compact sets.
Equations
- Filter.cocompact α = ⨅ s, ⨅ (_ : IsCompact s), Filter.principal sᶜ
Instances For
Filter.coclosedCompact
is the filter generated by complements to closed compact sets.
In a Hausdorff space, this is the same as Filter.cocompact
.
Equations
- Filter.coclosedCompact α = ⨅ s, ⨅ (_ : IsClosed s), ⨅ (_ : IsCompact s), Filter.principal sᶜ
Instances For
Sets that are contained in a compact set form a bornology. Its cobounded
filter is
Filter.cocompact
. See also Bornology.relativelyCompact
the bornology of sets with compact
closure.
Equations
- Bornology.inCompact α = { cobounded' := Filter.cocompact α, le_cofinite' := (_ : Filter.cocompact α ≤ Filter.cofinite) }
Instances For
If s
and t
are compact sets, then the set neighborhoods filter of s ×ˢ t
is the product of set neighborhoods filters for s
and t
.
For general sets, only the ≤
inequality holds, see nhdsSet_prod_le
.
The product of a neighborhood of s
and a neighborhood of t
is a neighborhood of s ×ˢ t
,
formulated in terms of a filter inequality.
If s
and t
are compact sets and n
is an open neighborhood of s × t
, then there exist
open neighborhoods u ⊇ s
and v ⊇ t
such that u × v ⊆ n
.
See also IsCompact.nhdsSet_prod_eq
.
Type class for compact spaces. Separation is sometimes included in the definition, especially in the French literature, but we do not include it here.
Instances
In a noncompact space,
Set.univ
is not a compact set.
α
is a noncompact topological space if it is not a compact space.
Instances
A compact discrete space is finite.
If α
is a compact space, then a locally finite family of sets of α
can have only finitely
many nonempty elements.
If α
is a compact space, then a locally finite family of nonempty sets of α
can have only
finitely many elements, Set.Finite
version.
If α
is a compact space, then a locally finite family of nonempty sets of α
can have only
finitely many elements, Fintype
version.
Equations
- LocallyFinite.fintypeOfCompact hf hne = Set.fintypeOfFiniteUniv (_ : Set.Finite Set.univ)
Instances For
The comap of the cocompact filter on β
by a continuous function f : α → β
is less than or
equal to the cocompact filter on α
.
This is a reformulation of the fact that images of compact sets are compact.
If X
is a compact topological space, then Prod.snd : X × Y → Y
is a closed map.
If f : α → β
is an Inducing
map, the image f '' s
of a set s
is compact
if and only if s
is compact.
If f : α → β
is an Embedding
, the image f '' s
of a set s
is compact
if and only if s
is compact.
The preimage of a compact set under an inducing map is a compact set.
The preimage of a compact set under a closed embedding is a compact set.
A closed embedding is proper, ie, inverse images of compact sets are contained in compacts.
Moreover, the preimage of a compact set is compact, see ClosedEmbedding.isCompact_preimage
.
Sets of subtype are compact iff the image under a coercion is.
Finite topological spaces are compact.
The product of two compact spaces is compact.
The disjoint union of two compact spaces is compact.
The coproduct of the cocompact filters on two topological spaces is the cocompact filter on their product.
Tychonoff's theorem: product of compact sets is compact.
Tychonoff's theorem formulated using Set.pi
: product of compact sets is compact.
Equations
Tychonoff's theorem formulated in terms of filters: Filter.cocompact
on an indexed product
type Π d, κ d
the Filter.coprodᵢ
of filters Filter.cocompact
on κ d
.