Theorems · Theorem · general topology

refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set

∀ {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} {s : Set X},
  IsClosed s →
    (∀ x ∈ s, (nhds x).HasBasis (p x) (B x)) →
      ∃ α c r, (∀ (a : α), c a ∈ s ∧ p (c a) (r a)) ∧ s ⊆ ⋃ a, B (c a) (r a) ∧ LocallyFinite fun a => B (c a) (r a)

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](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 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.

Defined in

Mathlib.Topology.Compactness.Paracompact

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceWeaklyLocallyCompactSpaceSigmaCompactSpaceT2Space