Properties of subsets of topological spaces
In this file we define various properties of subsets of a topological space, and some classes on topological spaces.
Main definitions
We define the following properties for sets in a topological space:
is_compact
: each open cover has a finite subcover. This is defined in mathlib using filters. The main property of a compact set isis_compact.elim_finite_subcover
.is_clopen
: a set that is both open and closed.is_irreducible
: a nonempty set that has contains no non-trivial pair of disjoint opens. See also the section below in the module doc.is_connected
: a nonempty set that has no non-trivial open partition. See also the section below in the module doc.connected_component
is the connected component of an element in the space.is_totally_disconnected
: all of its connected components are singletons.is_totally_separated
: any two points can be separated by two disjoint opens that cover the set.
For each of these definitions (except for is_clopen
), we also have a class stating that the whole
space satisfies that property:
compact_space
, irreducible_space
, connected_space
, totally_disconnected_space
,
totally_separated_space
.
Furthermore, we have two more classes:
locally_compact_space
: for every pointx
, every open neighborhood ofx
contains a compact neighborhood ofx
. The definition is formulated in terms of the neighborhood filter.sigma_compact_space
: a space that is the union of a countably many compact subspaces.
On the definition of irreducible and connected sets/spaces
In informal mathematics, irreducible and connected spaces are assumed to be nonempty.
We formalise the predicate without that assumption
as is_preirreducible
and is_preconnected
respectively.
In other words, the only difference is whether the empty space
counts as irreducible and/or connected.
There are good reasons to consider the empty space to be “too simple to be simple”
See also https://ncatlab.org/nlab/show/too+simple+to+be+simple,
and in particular
https://ncatlab.org/nlab/show/too+simple+to+be+simple#relationship_to_biased_definitions.
A set s
is compact if for every filter f
that contains s
,
every set of f
also meets every neighborhood of some a ∈ s
.
Equations
- is_compact s = ∀ ⦃f : filter α⦄ [_inst_2 : f.ne_bot], f ≤ 𝓟 s → (∃ (a : α) (H : a ∈ s), cluster_pt a f)
The complement to a compact set belongs to a filter f
if it belongs to each filter
𝓝 a ⊓ f
, a ∈ s
.
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 compact_iff_ultrafilter_le_nhds
.
For every open cover of a compact set, there exists a finite subcover.
For every family of closed sets whose intersection avoids a compact set, there exists a finite subfamily whose intersection avoids this compact set.
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 for every open cover of s
, there exists a finite subcover.
A set s
is compact if and only if
for every open cover of s
, there exists a finite subcover.
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
.
filter.cocompact
is the filter generated by complements to compact sets.
Equations
- filter.cocompact α = ⨅ (s : set α) (hs : is_compact s), 𝓟 sᶜ
nhds_contain_boxes s t
means that any open neighborhood of s × t
in α × β
includes
a product of an open neighborhood of s
by an open neighborhood of t
.
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
.
- compact_univ : is_compact set.univ
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
- fintype.compact_space
- prod.compact_space
- sum.compact_space
- pi.compact
- quot.compact_space
- quotient.compact_space
- prime_spectrum.compact_space
- topological_space.nonempty_compacts.to_compact_space
- set.Icc.compact_space
- CompHaus.compact_space
- Compactum.compact_space
- Profinite.compact_space
- emetric.closeds.compact_space
- emetric.nonempty_compacts.compact_space
- Gromov_Hausdorff.compact_space_optimal_GH_coupling
- Gromov_Hausdorff.rep_GH_space_compact_space
- ultrafilter_compact
- stone_cech.compact_space
If X is is_compact then pr₂ : X × Y → Y is a closed map
Finite topological spaces are compact.
The product of two compact spaces is compact.
The disjoint union of two compact spaces is compact.
Tychonoff's theorem
A version of Tychonoff's theorem that uses set.pi
.
- local_compact_nhds : ∀ (x : α) (n : set α), n ∈ 𝓝 x → (∃ (s : set α) (H : s ∈ 𝓝 x), s ⊆ n ∧ is_compact s)
There are various definitions of "locally compact space" in the literature, which agree for
Hausdorff spaces but not in general. This one is the precise condition on X needed for the
evaluation map C(X, Y) × X → Y
to be continuous for all Y
when C(X, Y)
is given the
compact-open topology.
A reformulation of the definition of locally compact space: In a locally compact space,
every open set containing x
has a compact subset containing x
in its interior.
- exists_compact_covering : ∃ (K : ℕ → set α), (∀ (n : ℕ), is_compact (K n)) ∧ (⋃ (n : ℕ), K n) = set.univ
A σ-compact space is a space that is the union of a countable collection of compact subspaces.
Note that a locally compact separable T₂ space need not be σ-compact.
The sequence can be extracted using topological_space.compact_covering
.
An arbitrary compact covering of a σ-compact space.
A preirreducible set s
is one where there is no non-trivial pair of disjoint opens on s
.
An irreducible set s
is one that is nonempty and
where there is no non-trivial pair of disjoint opens on s
.
Equations
- is_irreducible s = (s.nonempty ∧ is_preirreducible s)
A maximal irreducible set that contains a given point.
Equations
- is_preirreducible_univ : is_preirreducible set.univ
A preirreducible space is one where there is no non-trivial pair of disjoint opens.
- to_preirreducible_space : preirreducible_space α
- to_nonempty : nonempty α
An irreducible space is one that is nonempty and where there is no non-trivial pair of disjoint opens.
A set s
is irreducible if and only if
for every finite collection of open sets all of whose members intersect s
,
s
also intersects the intersection of the entire collection
(i.e., there is an element of s
contained in every member of the collection).
A set is preirreducible if and only if for every cover by two closed sets, it is contained in one of the two covering sets.
A set is irreducible if and only if for every cover by a finite collection of closed sets, it is contained in one of the members of the collection.
A connected set is one that is nonempty and where there is no non-trivial open partition.
Equations
- is_connected s = (s.nonempty ∧ is_preconnected s)
If any point of a set is joined to a fixed point by a preconnected subset, then the original set is preconnected as well.
If any two points of a set are contained in a preconnected subset, then the original set is preconnected as well.
A union of a family of preconnected sets with a common point is preconnected as well.
The connected component of a point is the maximal connected set that contains this point.
Equations
- connected_component x = ⋃₀{s : set α | is_preconnected s ∧ x ∈ s}
The connected component of a point inside a set.
Equations
- is_preconnected_univ : is_preconnected set.univ
A preconnected space is one where there is no non-trivial open partition.
- to_preconnected_space : preconnected_space α
- to_nonempty : nonempty α
A connected space is a nonempty one where there is no non-trivial open partition.
A set s
is preconnected if and only if
for every cover by two open sets that are disjoint on s
,
it is contained in one of the two covering sets.
A set s
is connected if and only if
for every cover by a finite collection of open sets that are pairwise disjoint on s
,
it is contained in one of the members of the collection.
Preconnected sets are either contained in or disjoint to any given clopen set.
A set s
is preconnected if and only if
for every cover by two closed sets that are disjoint on s
,
it is contained in one of the two covering sets.
A closed set s
is preconnected if and only if
for every cover by two closed sets that are disjoint,
it is contained in one of the two covering sets.
The connected component of a point is always a subset of the intersection of all its clopen neighbourhoods.
A set is called totally disconnected if all of its connected components are singletons.
Equations
- is_totally_disconnected s = ∀ (t : set α), t ⊆ s → is_preconnected t → subsingleton ↥t
- is_totally_disconnected_univ : is_totally_disconnected set.univ
A space is totally disconnected if all of its connected components are singletons.
A set s
is called totally separated if any two points of this set can be separated
by two disjoint open sets covering s
.
- is_totally_separated_univ : is_totally_separated set.univ
A space is totally separated if any two points can be separated by two disjoint open sets covering the whole space.