Theorems · Theorem · general topology

refinement_of_locallyCompact_sigmaCompact_of_nhds_basis

∀ {X : Type v} [inst : TopologicalSpace X] [WeaklyLocallyCompactSpace X] [SigmaCompactSpace X] [T2Space X]
  {ι : X → Type u} {p : (x : X) → ι x → Prop} {B : (x : X) → ι x → Set X},
  (∀ (x : X), (nhds x).HasBasis (p x) (B x)) →
    ∃ α c r, (∀ (a : α), p (c a) (r a)) ∧ ⋃ a, B (c a) (r a) = Set.univ ∧ LocallyFinite fun a => B (c a) (r a)

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](https://ncatlab.org/) proofs: * [locally compact and sigma compact spaces are paracompact](https://ncatlab.org/nlab/show/locally+compact+and+sigma-compact+spaces+are+paracompact); * [open cover of smooth manifold admits locally finite refinement by closed balls](https://ncatlab.org/nlab/show/partition+of+unity#ExistenceOnSmoothManifolds). 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.

Defined in

Mathlib.Topology.Compactness.Paracompact

Cited by

0 results in Mathlib

Foundations

Depth 88 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceWeaklyLocallyCompactSpaceSigmaCompactSpaceT2Space