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_locallyCompact_sigmaCompact
. Moreover, we can choose a locally finite refinement with sets in a given collection of filter bases of𝓝 x
,x : X
, seerefinement_of_locallyCompact_sigmaCompact_of_nhds_basis
. For example, in a proper metric space every open covering⋃ i, s i
admits 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
EMetricSpace
is a paracompact space, see instanceEMetric.instParacompactSpace
inTopology/EMetricSpace/Paracompact
.
TODO #
Prove (some of) Michael's theorems.
Tags #
compact space, paracompact space, locally finite covering
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 ParacompactSpace.{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
.
 locallyFinite_refinement : ∀ (α : Type v) (s : α → Set X), (∀ (a : α), IsOpen (s a)) → ⋃ (a : α), s a = Set.univ → ∃ (β : Type v) (t : β → Set X) (_ : ∀ (b : β), IsOpen (t b)) (_ : ⋃ (b : β), t b = Set.univ), LocallyFinite t ∧ ∀ (b : β), ∃ (a : α), t b ⊆ s a
Every open cover of a paracompact space assumes a locally finite refinement.
Instances
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.
The product of a compact space and a paracompact space is a paracompact space. The formalization is based on https://dantopology.wordpress.com/2009/10/24/compactxparacompactisparacompact/ with some minor modifications.
This version assumes that X
in X × Y
is compact and Y
is paracompact, see next lemma for the
other case.
Equations
 (_ : ParacompactSpace (X × Y)) = (_ : ParacompactSpace (X × Y))
Equations
 (_ : ParacompactSpace (X × Y)) = (_ : ParacompactSpace (X × Y))
A compact space is paracompact.
Equations
 (_ : ParacompactSpace X) = (_ : ParacompactSpace X)
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
fun 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.HasBasis.restrict_subset
or a similar lemma, see
the proof of paracompact_of_locallyCompact_sigmaCompact
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_locallyCompact_sigmaCompact_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 fun 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.HasBasis.restrict_subset
or a similar lemma, see
the proof of paracompact_of_locallyCompact_sigmaCompact
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_locallyCompact_sigmaCompact_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_locallyCompact_sigmaCompact_of_nhds_basis
for a more precise statement.
Equations
 (_ : ParacompactSpace X) = (_ : ParacompactSpace X)