English
Same as before: there exists a partition of unity subordinate to a locally finite open cover of a closed set in a normal space.
Русский
То же: существует разложение по единице подпадающее под локально конечное открытое покрытие закрытого множества в нормальном пространстве.
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
/-- A variation of **Urysohn's lemma**.
In a locally compact T2 space `X`, for a compact set `t` and a finite family of open sets `{s i}_i`
such that `t ⊆ ⋃ i, s i`, there is a family of compactly supported continuous functions `{f i}_i`
supported in `s i`, `∑ i, f i x = 1` on `t` and `0 ≤ f i x ≤ 1`. -/
theorem exists_continuous_sum_one_of_isOpen_isCompact [T2Space X] [LocallyCompactSpace X] {n : ℕ} {t : Set X}
{s : Fin n → Set X} (hs : ∀ (i : Fin n), IsOpen (s i)) (htcp : IsCompact t) (hst : t ⊆ ⋃ i, s i) :
∃ f : Fin n → C(X, ℝ),
(∀ (i : Fin n), tsupport (f i) ⊆ s i) ∧
EqOn (∑ i, f i) 1 t ∧
(∀ (i : Fin n), ∀ (x : X), f i x ∈ Icc (0 : ℝ) 1) ∧ (∀ (i : Fin n), HasCompactSupport (f i)) :=
by
obtain ⟨f, hfsub, hfcp⟩ :=
PartitionOfUnity.exists_isSubordinate_of_locallyFinite_t2space htcp s hs (locallyFinite_of_finite _) hst
use f
refine ⟨fun i ↦ hfsub i, ?_, ?_, fun i => hfcp i⟩
· intro x hx
simp only [Finset.sum_apply, Pi.one_apply]
have h := f.sum_eq_one' x hx
rw [finsum_eq_sum (fun i => (f.toFun i) x)
(Finite.subset finite_univ (subset_univ (support fun i ↦ (f.toFun i) x)))] at h
rwa [Fintype.sum_subset (by simp)] at h
intro i x
exact ⟨f.nonneg i x, PartitionOfUnity.le_one f i x⟩
