English
In a locally compact sigma-compact Hausdorff space, given an open cover of a closed set with a basis of neighborhoods, there exists a locally finite refinement by sets contained in the corresponding basis elements.
Русский
В локально компактном σ-компактном пространстве Хаусдорфа для открытого покрытия замкнутого множества с базисом окрестностей существует локально конечное уточнение наборами, вложенными в соответствующие элементы базиса.
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, 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`. -/
theorem refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set [WeaklyLocallyCompactSpace X] [SigmaCompactSpace X]
[T2Space X] {ι : X → Type u} {p : ∀ x, ι x → Prop} {B : ∀ x, ι x → Set X} {s : Set X} (hs : IsClosed s)
(hB : ∀ x ∈ s, (𝓝 x).HasBasis (p x) (B x)) :
∃ (α : Type v) (c : α → X) (r : ∀ a, ι (c a)),
(∀ a, c a ∈ s ∧ p (c a) (r a)) ∧ (s ⊆ ⋃ a, B (c a) (r a)) ∧ LocallyFinite fun a ↦ B (c a) (r a) :=
by
classical
-- For technical reasons we prepend two empty sets to the sequence `CompactExhaustion.choice X`
set K' : CompactExhaustion X := CompactExhaustion.choice X
set K : CompactExhaustion X := K'.shiftr.shiftr
set Kdiff := fun n ↦
K (n + 1) \
interior
(K n)
-- Now we restate some properties of `CompactExhaustion` for `K`/`Kdiff`
have hKcov : ∀ x, x ∈ Kdiff (K'.find x + 1) := fun x ↦ by
simpa only [K'.find_shiftr] using diff_subset_diff_right interior_subset (K'.shiftr.mem_diff_shiftr_find x)
have Kdiffc : ∀ n, IsCompact (Kdiff n ∩ s) := fun n ↦ ((K.isCompact _).diff isOpen_interior).inter_right hs
have : ∀ (n) (x : ↑(Kdiff (n + 1) ∩ s)), (K n)ᶜ ∈ 𝓝 (x : X) := fun n x ↦
(K.isClosed n).compl_mem_nhds fun hx' ↦ x.2.1.2 <| K.subset_interior_succ _ hx'
choose! r hrp hr using fun n (x : ↑(Kdiff (n + 1) ∩ s)) ↦ (hB x x.2.2).mem_iff.1 (this n x)
have hxr : ∀ (n x) (hx : x ∈ Kdiff (n + 1) ∩ s), B x (r n ⟨x, hx⟩) ∈ 𝓝 x := fun n x hx ↦
(hB x hx.2).mem_of_mem (hrp _ ⟨x, hx⟩)
choose T hT using fun n ↦ (Kdiffc (n + 1)).elim_nhds_subcover' _ (hxr n)
set T' : ∀ n, Set ↑(Kdiff (n + 1) ∩ s) := fun n ↦ T n
refine ⟨Σ n, T' n, fun a ↦ a.2, fun a ↦ r a.1 a.2, ?_, ?_, ?_⟩
· rintro ⟨n, x, hx⟩
exact ⟨x.2.2, hrp _ _⟩
· refine fun x hx ↦ mem_iUnion.2 ?_
rcases mem_iUnion₂.1 (hT _ ⟨hKcov x, hx⟩) with ⟨⟨c, hc⟩, hcT, hcx⟩
exact ⟨⟨_, ⟨c, hc⟩, hcT⟩, hcx⟩
· intro x
refine ⟨interior (K (K'.find x + 3)), IsOpen.mem_nhds isOpen_interior (K.subset_interior_succ _ (hKcov x).1), ?_⟩
have : (⋃ k ≤ K'.find x + 2, range (Sigma.mk k) : Set (Σ n, T' n)).Finite :=
(finite_le_nat _).biUnion fun k _ ↦ finite_range _
apply this.subset
rintro ⟨k, c, hc⟩
simp only [mem_iUnion, mem_setOf_eq, Subtype.coe_mk]
rintro ⟨x, hxB : x ∈ B c (r k c), hxK⟩
refine ⟨k, ?_, ⟨c, hc⟩, rfl⟩
have := (mem_compl_iff _ _).1 (hr k c hxB)
contrapose! this with hnk
exact K.subset hnk (interior_subset hxK)
