# 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`

, see`refinement_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 instance`EMetric.instParacompactSpace`

in`Topology/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

Every open cover of a paracompact space assumes a locally finite refinement.

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/compact-x-paracompact-is-paracompact/ 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

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

A compact space is paracompact.

## Equations

- ⋯ = ⋯

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

- ⋯ = ⋯

**Dieudonné's theorem**: a paracompact Hausdorff space is normal.
Formalization is based on the proof
at ncatlab.

## Equations

- ⋯ = ⋯