Properties of subsets of topological spaces
Main definitions
compact
, is_clopen
, is_irreducible
, is_connected
, is_totally_disconnected
,
is_totally_separated
TODO: write better docs
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 ≤ filter.principal 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
twithin
ssuch 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.
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
.
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
.
- 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
- 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.
Equations
The product of two compact spaces is compact.
Equations
The disjoint union of two compact spaces is compact.
Equations
Tychonoff's theorem
A version of Tychonoff's theorem that uses set.pi
.
Equations
- pi.compact = _
Equations
Equations
- local_compact_nhds : ∀ (x : α) (n : set α), n ∈ nhds x → (∃ (s : set α) (H : s ∈ nhds 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.
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.
Equations
- _ = _
Equations
- _ = _
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.
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.
Equations
- _ = _