English
In a weakly locally compact, sigma-compact, T2 space, given a HasBasis of neighborhoods B_x, there exists a refinement by sets B(c a)(r a) that still covers X and is locally finite.
Русский
В слабой локально компактной σ-компактной топологической пространстве существует уточнение открытого базиса, сохраняющее покрытие и локальную конечность.
LaTeX
$$$ \\exists α, \\exists c : α \\to X, \\exists r : \\forall a, ι(c a), \\Big( \\forall a, p(c a)(r a) \\Big) \\land \\Big( \\bigcup_a B(c a)(r a) = univ \\Big) \\land LocallyFinite(\\lambda a, B(c a)(r a)) $$$
Lean4
/-- 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`. -/
theorem refinement_of_locallyCompact_sigmaCompact_of_nhds_basis [WeaklyLocallyCompactSpace X] [SigmaCompactSpace X]
[T2Space X] {ι : X → Type u} {p : ∀ x, ι x → Prop} {B : ∀ x, ι x → Set X} (hB : ∀ x, (𝓝 x).HasBasis (p x) (B x)) :
∃ (α : Type v) (c : α → X) (r : ∀ a, ι (c a)),
(∀ a, p (c a) (r a)) ∧ ⋃ a, B (c a) (r a) = univ ∧ LocallyFinite fun a ↦ B (c a) (r a) :=
let ⟨α, c, r, hp, hU, hfin⟩ :=
refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set isClosed_univ fun x _ ↦ hB x
⟨α, c, r, fun a ↦ (hp a).2, univ_subset_iff.1 hU, hfin⟩
-- See note [lower instance priority]
