English
In a normal space, given a closed s and a locally finite open cover U of s with hU, there exists f which is subordinate to U.
Русский
В нормальном пространстве, при задании закрытого s и локально конечного открытого покрытия U разложения по единице существует f, подпадающее под U.
LaTeX
$$[NormalSpace X] IsClosed s → (U : ι → Set X) → (ho : ∀ i, IsOpen (U i)) → LocallyFinite U → (hU : s ⊆ ⋃ i, U i) → ∃ f : PartitionOfUnity ι X s, f.IsSubordinate U$$
Lean4
/-- If `X` is a locally compact T2 topological space and `U` is a locally finite open covering of a
compact set `s`, then there exists a `PartitionOfUnity ι X s` that is subordinate to `U`. -/
theorem exists_isSubordinate_of_locallyFinite_t2space [LocallyCompactSpace X] [T2Space X] (hs : IsCompact s)
(U : ι → Set X) (ho : ∀ i, IsOpen (U i)) (hf : LocallyFinite U) (hU : s ⊆ ⋃ i, U i) :
∃ f : PartitionOfUnity ι X s, f.IsSubordinate U ∧ ∀ i, HasCompactSupport (f i) :=
let ⟨f, hfsub, hfcp⟩ := BumpCovering.exists_isSubordinate_hasCompactSupport_of_locallyFinite_t2space hs U ho hf hU
⟨f.toPartitionOfUnity, hfsub.toPartitionOfUnity, fun i =>
IsCompact.of_isClosed_subset (hfcp i) isClosed_closure <| closure_mono (f.support_toPartitionOfUnity_subset i)⟩
