Paracompact topological spaces #
A topological space X
is said to be paracompact if every open covering of X
admits a locally
finite refinement.
The definition requires that each set of the new covering is a subset of one of the sets of the
initial covering. However, one can ensure that each open covering s : ι → set X
admits a precise
locally finite refinement, i.e., an open covering t : ι → set X
with the same index set such that
∀ i, t i ⊆ s i
, see lemma precise_refinement
. We also provide a convenience lemma
precise_refinement_set
that deals with open coverings of a closed subset of X
instead of the
whole space.
We also prove the following facts.
-
Every compact space is paracompact, see instance
paracompact_of_compact
. -
A locally compact sigma compact Hausdorff space is paracompact, see instance
paracompact_of_locally_compact_sigma_compact
. Moreover, we can choose a locally finite refinement with sets in a given collection of filter bases of𝓝 x,
x : X, see
refinement_of_locally_compact_sigma_compact_of_nhds_basis. For example, in a proper metric space every open covering
⋃ i, s iadmits a refinement
⋃ i, metric.ball (c i) (r i)`. -
Every paracompact Hausdorff space is normal. This statement is not an instance to avoid loops in the instance graph.
-
Every
emetric_space
is a paracompact space, see instanceemetric_space.paracompact_space
intopology/metric_space/emetric_space
.
TODO #
Prove (some of) Michael's theorems.
Tags #
compact space, paracompact space, locally finite covering
- locally_finite_refinement : ∀ (α : Type ?) (s : α → set X), (∀ (a : α), is_open (s a)) → (⋃ (a : α), s a) = set.univ → (∃ (β : Type ?) (t : β → set X) (ho : ∀ (b : β), is_open (t b)) (hc : (⋃ (b : β), t b) = set.univ), locally_finite t ∧ ∀ (b : β), ∃ (a : α), t b ⊆ s a)
A topological space is called paracompact, if every open covering of this space admits a locally
finite refinement. We use the same universe for all types in the definition to avoid creating a
class like paracompact_space.{u v}
. Due to lemma precise_refinement
below, every open covering
s : α → set X
indexed on α : Type v
has a precise locally finite refinement, i.e., a locally
finite refinement t : α → set X
indexed on the same type such that each ∀ i, t i ⊆ s i
.
Instances of this typeclass
Any open cover of a paracompact space has a locally finite precise refinement, that is, one indexed on the same type with each open set contained in the corresponding original one.
In a paracompact space, every open covering of a closed set admits a locally finite refinement indexed by the same type.
A compact space is paracompact.
Let X
be a locally compact sigma compact Hausdorff topological space, let s
be a closed set
in X
. Suppose that for each x ∈ s
the sets B x : ι x → set X
with the predicate
p x : ι x → Prop
form a basis of the filter 𝓝 x
. Then there exists a locally finite covering
λ i, B (c i) (r i)
of s
such that all “centers” c i
belong to s
and each r i
satisfies
p (c i)
.
The notation is inspired by the case B x r = metric.ball x r
but the theorem applies to
nhds_basis_opens
as well. If the covering must be subordinate to some open covering of s
, then
the user should use a basis obtained by filter.has_basis.restrict_subset
or a similar lemma, see
the proof of paracompact_of_locally_compact_sigma_compact
for an example.
The formalization is based on two ncatlab proofs:
- locally compact and sigma compact spaces are paracompact;
- open cover of smooth manifold admits locally finite refinement by closed balls.
See also refinement_of_locally_compact_sigma_compact_of_nhds_basis
for a version of this lemma
dealing with a covering of the whole space.
In most cases (namely, if B c r ∪ B c r'
is again a set of the form B c r''
) it is possible
to choose α = X
. This fact is not yet formalized in mathlib
.
Let X
be a locally compact sigma compact Hausdorff topological space. Suppose that for each
x
the sets B x : ι x → set X
with the predicate p x : ι x → Prop
form a basis of the filter
𝓝 x
. Then there exists a locally finite covering λ i, B (c i) (r i)
of X
such that each r i
satisfies p (c i)
The notation is inspired by the case B x r = metric.ball x r
but the theorem applies to
nhds_basis_opens
as well. If the covering must be subordinate to some open covering of s
, then
the user should use a basis obtained by filter.has_basis.restrict_subset
or a similar lemma, see
the proof of paracompact_of_locally_compact_sigma_compact
for an example.
The formalization is based on two ncatlab proofs:
- locally compact and sigma compact spaces are paracompact;
- open cover of smooth manifold admits locally finite refinement by closed balls.
See also refinement_of_locally_compact_sigma_compact_of_nhds_basis_set
for a version of this lemma
dealing with a covering of a closed set.
In most cases (namely, if B c r ∪ B c r'
is again a set of the form B c r''
) it is possible
to choose α = X
. This fact is not yet formalized in mathlib
.
A locally compact sigma compact Hausdorff space is paracompact. See also
refinement_of_locally_compact_sigma_compact_of_nhds_basis
for a more precise statement.