Continuous partition of unity

In this file we define PartitionOfUnity (ι X : Type*) [TopologicalSpace X] (s : Set X := univ) to be a continuous partition of unity on s indexed by ι. More precisely, f : PartitionOfUnity ι X s is a collection of continuous functions f i : C(X, ℝ), i : ι, such that

• the supports of f i form a locally finite family of sets;
• each f i is nonnegative;
• ∑ᶠ i, f i x = 1 for all x ∈ s;
• ∑ᶠ i, f i x ≤ 1 for all x : X.

In the case s = univ the last assumption follows from the previous one but it is convenient to have this assumption in the case s ≠ univ.

We also define a bump function covering, BumpCovering (ι X : Type*) [TopologicalSpace X] (s : Set X := univ), to be a collection of functions f i : C(X, ℝ), i : ι, such that

• the supports of f i form a locally finite family of sets;
• each f i is nonnegative;
• for each x ∈ s there exists i : ι such that f i y = 1 in a neighborhood of x.

The term is motivated by the smooth case.

If f is a bump function covering indexed by a linearly ordered type, then g i x = f i x * ∏ᶠ j < i, (1 - f j x) is a partition of unity, see BumpCovering.toPartitionOfUnity. Note that only finitely many terms 1 - f j x are not equal to one, so this product is well-defined.

Note that g i x = ∏ᶠ j ≤ i, (1 - f j x) - ∏ᶠ j < i, (1 - f j x), so most terms in the sum ∑ᶠ i, g i x cancel, and we get ∑ᶠ i, g i x = 1 - ∏ᶠ i, (1 - f i x), and the latter product equals zero because one of f i x is equal to one.

We say that a partition of unity or a bump function covering f is subordinate to a family of sets U i, i : ι, if the closure of the support of each f i is included in U i. We use Urysohn's Lemma to prove that a locally finite open covering of a normal topological space admits a subordinate bump function covering (hence, a subordinate partition of unity), see BumpCovering.exists_isSubordinate_of_locallyFinite. If X is a paracompact space, then any open covering admits a locally finite refinement, hence it admits a subordinate bump function covering and a subordinate partition of unity, see BumpCovering.exists_isSubordinate.

We also provide two slightly more general versions of these lemmas, BumpCovering.exists_isSubordinate_of_locallyFinite_of_prop and BumpCovering.exists_isSubordinate_of_prop, to be used later in the construction of a smooth partition of unity.

Implementation notes

Most (if not all) books only define a partition of unity of the whole space. However, quite a few proofs only deal with f i such that tsupport (f i) meets a specific closed subset, and it is easier to formalize these proofs if we don't have other functions right away.

We use WellOrderingRel j i instead of j < i in the definition of BumpCovering.toPartitionOfUnity to avoid a [LinearOrder ι] assumption. While WellOrderingRel j i is a well order, not only a strict linear order, we never use this property.

Tags

partition of unity, bump function, Urysohn's lemma, normal space, paracompact space

structure PartitionOfUnity (ι : Type u_1) (X : Type u_2) [TopologicalSpace X] (s : optParam (Set X) Set.univ) : Type (max u_1 u_2)

• toFun : ι → C(X, ℝ)
• locallyFinite' : LocallyFinite fun i => Function.support ↑(PartitionOfUnity.toFun s✝ s i)
• nonneg' : 0 ≤ s.toFun
• sum_eq_one' : ∀ (x : X), x ∈ s✝ → ∑ᶠ (i : ι), ↑(PartitionOfUnity.toFun s✝ s i) x = 1
• sum_le_one' : ∀ (x : X), ∑ᶠ (i : ι), ↑(PartitionOfUnity.toFun s✝ s i) x ≤ 1

A continuous partition of unity on a set s : Set X is a collection of continuous functions f i such that

• the supports of f i form a locally finite family of sets, i.e., for every point x : X there exists a neighborhood U ∋ x such that all but finitely many functions f i are zero on U;
• the functions f i are nonnegative;
• the sum ∑ᶠ i, f i x is equal to one for every x ∈ s and is less than or equal to one otherwise.

If X is a normal paracompact space, then PartitionOfUnity.exists_isSubordinate guarantees that for every open covering U : Set (Set X) of s there exists a partition of unity that is subordinate to U.

structure BumpCovering (ι : Type u_1) (X : Type u_2) [TopologicalSpace X] (s : optParam (Set X) Set.univ) : Type (max u_1 u_2)

• toFun : ι → C(X, ℝ)
• locallyFinite' : LocallyFinite fun i => Function.support ↑(BumpCovering.toFun s✝ s i)
• nonneg' : 0 ≤ s.toFun
• le_one' : s.toFun ≤ 1
• eventuallyEq_one' : ∀ (x : X), x ∈ s✝ → ∃ i, ↑(BumpCovering.toFun s✝ s i) =ᶠ[nhds x] 1

A BumpCovering ι X s is an indexed family of functions f i, i : ι, such that

• the supports of f i form a locally finite family of sets, i.e., for every point x : X there exists a neighborhood U ∋ x such that all but finitely many functions f i are zero on U;
• for all i, x we have 0 ≤ f i x ≤ 1;
• each point x ∈ s belongs to the interior of {x | f i x = 1} for some i.

One of the main use cases for a BumpCovering is to define a PartitionOfUnity, see BumpCovering.toPartitionOfUnity, but some proofs can directly use a BumpCovering instead of a PartitionOfUnity.

If X is a normal paracompact space, then BumpCovering.exists_isSubordinate guarantees that for every open covering U : Set (Set X) of s there exists a BumpCovering of s that is subordinate to U.

instance PartitionOfUnity.instFunLikePartitionOfUnityContinuousMapRealToTopologicalSpaceToUniformSpacePseudoMetricSpace {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} : FunLike (PartitionOfUnity ι X s) ι fun x => C(X, ℝ)

theorem PartitionOfUnity.locallyFinite {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : PartitionOfUnity ι X s) : LocallyFinite fun i => Function.support ↑(↑f i)

theorem PartitionOfUnity.locallyFinite_tsupport {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : PartitionOfUnity ι X s) : LocallyFinite fun i => tsupport ↑(↑f i)

theorem PartitionOfUnity.nonneg {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : PartitionOfUnity ι X s) (i : ι) (x : X) : 0 ≤ ↑(↑f i) x

theorem PartitionOfUnity.sum_eq_one {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : PartitionOfUnity ι X s) {x : X} (hx : x ∈ s) : ∑ᶠ (i : ι), ↑(↑f i) x = 1

theorem PartitionOfUnity.exists_pos {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : PartitionOfUnity ι X s) {x : X} (hx : x ∈ s) : ∃ i, 0 < ↑(↑f i) x

If f is a partition of unity on s, then for every x ∈ s there exists an index i such that 0 < f i x.

theorem PartitionOfUnity.sum_le_one {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : PartitionOfUnity ι X s) (x : X) : ∑ᶠ (i : ι), ↑(↑f i) x ≤ 1

theorem PartitionOfUnity.sum_nonneg {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : PartitionOfUnity ι X s) (x : X) : 0 ≤ ∑ᶠ (i : ι), ↑(↑f i) x

theorem PartitionOfUnity.le_one {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : PartitionOfUnity ι X s) (i : ι) (x : X) : ↑(↑f i) x ≤ 1

theorem PartitionOfUnity.continuous_smul {ι : Type u} {X : Type v} [TopologicalSpace X] {E : Type u_1} [AddCommMonoid E] [SMulWithZero ℝ E] [TopologicalSpace E] [ContinuousSMul ℝ E] {s : Set X} (f : PartitionOfUnity ι X s) {g : X → E} {i : ι} (hg : ∀ (x : X), x ∈ tsupport ↑(↑f i) → ContinuousAt g x) : Continuous fun x => ↑(↑f i) x • g x

If f is a partition of unity on s : Set X and g : X → E is continuous at every point of the topological support of some f i, then fun x ↦ f i x • g x is continuous on the whole space.

theorem PartitionOfUnity.continuous_finsum_smul {ι : Type u} {X : Type v} [TopologicalSpace X] {E : Type u_1} [AddCommMonoid E] [SMulWithZero ℝ E] [TopologicalSpace E] [ContinuousSMul ℝ E] {s : Set X} (f : PartitionOfUnity ι X s) [ContinuousAdd E] {g : ι → X → E} (hg : ∀ (i : ι) (x : X), x ∈ tsupport ↑(↑f i) → ContinuousAt (g i) x) : Continuous fun x => ∑ᶠ (i : ι), ↑(↑f i) x • g i x

If f is a partition of unity on a set s : Set X and g : ι → X → E is a family of functions such that each g i is continuous at every point of the topological support of f i, then the sum fun x ↦ ∑ᶠ i, f i x • g i x is continuous on the whole space.

def PartitionOfUnity.IsSubordinate {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : PartitionOfUnity ι X s) (U : ι → Set X) : Prop

A partition of unity f i is subordinate to a family of sets U i indexed by the same type if for each i the closure of the support of f i is a subset of U i.

theorem PartitionOfUnity.exists_finset_nhd_support_subset {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} {f : PartitionOfUnity ι X s} {U : ι → Set X} (hso : PartitionOfUnity.IsSubordinate f U) (ho : ∀ (i : ι), IsOpen (U i)) (x : X) : ∃ is n x x, ∀ (z : X), z ∈ n → (Function.support fun i => ↑(↑f i) z) ⊆ ↑is

theorem PartitionOfUnity.IsSubordinate.continuous_finsum_smul {ι : Type u} {X : Type v} [TopologicalSpace X] {E : Type u_1} [AddCommMonoid E] [SMulWithZero ℝ E] [TopologicalSpace E] [ContinuousSMul ℝ E] {s : Set X} {f : PartitionOfUnity ι X s} [ContinuousAdd E] {U : ι → Set X} (ho : ∀ (i : ι), IsOpen (U i)) (hf : PartitionOfUnity.IsSubordinate f U) {g : ι → X → E} (hg : ∀ (i : ι), ContinuousOn (g i) (U i)) : Continuous fun x => ∑ᶠ (i : ι), ↑(↑f i) x • g i x

If f is a partition of unity that is subordinate to a family of open sets U i and g : ι → X → E is a family of functions such that each g i is continuous on U i, then the sum fun x ↦ ∑ᶠ i, f i x • g i x is a continuous function.

instance BumpCovering.instFunLikeBumpCoveringContinuousMapRealToTopologicalSpaceToUniformSpacePseudoMetricSpace {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} : FunLike (BumpCovering ι X s) ι fun x => C(X, ℝ)

theorem BumpCovering.locallyFinite {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) : LocallyFinite fun i => Function.support ↑(↑f i)

theorem BumpCovering.locallyFinite_tsupport {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) : LocallyFinite fun i => tsupport ↑(↑f i)

theorem BumpCovering.point_finite {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (x : X) : Set.Finite {i | ↑(↑f i) x ≠ 0}

theorem BumpCovering.nonneg {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) (x : X) : 0 ≤ ↑(↑f i) x

theorem BumpCovering.le_one {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) (x : X) : ↑(↑f i) x ≤ 1

def BumpCovering.single {ι : Type u} {X : Type v} [TopologicalSpace X] (i : ι) (s : Set X) : BumpCovering ι X s

A BumpCovering that consists of a single function, uniformly equal to one, defined as an example for Inhabited instance.

@[simp]

theorem BumpCovering.coe_single {ι : Type u} {X : Type v} [TopologicalSpace X] (i : ι) (s : Set X) : ↑(BumpCovering.single i s) = Pi.single i 1

instance BumpCovering.instInhabitedBumpCovering {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} [Inhabited ι] : Inhabited (BumpCovering ι X s)

def BumpCovering.IsSubordinate {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (U : ι → Set X) : Prop

A collection of bump functions f i is subordinate to a family of sets U i indexed by the same type if for each i the closure of the support of f i is a subset of U i.

theorem BumpCovering.IsSubordinate.mono {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} {f : BumpCovering ι X s} {U : ι → Set X} {V : ι → Set X} (hU : BumpCovering.IsSubordinate f U) (hV : ∀ (i : ι), U i ⊆ V i) : BumpCovering.IsSubordinate f V

theorem BumpCovering.exists_isSubordinate_of_locallyFinite_of_prop {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} [NormalSpace X] (p : (X → ℝ) → Prop) (h01 : ∀ (s t : Set X), IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ↑f ∧ Set.EqOn (↑f) 0 s ∧ Set.EqOn (↑f) 1 t ∧ ∀ (x : X), ↑f x ∈ Set.Icc 0 1) (hs : IsClosed s) (U : ι → Set X) (ho : ∀ (i : ι), IsOpen (U i)) (hf : LocallyFinite U) (hU : s ⊆ ⋃ (i : ι), U i) : ∃ f, ((i : ι) → p ↑(↑f i)) ∧ BumpCovering.IsSubordinate f U

If X is a normal topological space and U i, i : ι, is a locally finite open covering of a closed set s, then there exists a BumpCovering ι X s that is subordinate to U. If X is a paracompact space, then the assumption hf : LocallyFinite U can be omitted, see BumpCovering.exists_isSubordinate. This version assumes that p : (X → ℝ) → Prop is a predicate that satisfies Urysohn's lemma, and provides a BumpCovering such that each function of the covering satisfies p.

theorem BumpCovering.exists_isSubordinate_of_locallyFinite {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} [NormalSpace X] (hs : IsClosed s) (U : ι → Set X) (ho : ∀ (i : ι), IsOpen (U i)) (hf : LocallyFinite U) (hU : s ⊆ ⋃ (i : ι), U i) : ∃ f, BumpCovering.IsSubordinate f U

If X is a normal topological space and U i, i : ι, is a locally finite open covering of a closed set s, then there exists a BumpCovering ι X s that is subordinate to U. If X is a paracompact space, then the assumption hf : LocallyFinite U can be omitted, see BumpCovering.exists_isSubordinate.

theorem BumpCovering.exists_isSubordinate_of_prop {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} [NormalSpace X] [ParacompactSpace X] (p : (X → ℝ) → Prop) (h01 : ∀ (s t : Set X), IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ↑f ∧ Set.EqOn (↑f) 0 s ∧ Set.EqOn (↑f) 1 t ∧ ∀ (x : X), ↑f x ∈ Set.Icc 0 1) (hs : IsClosed s) (U : ι → Set X) (ho : ∀ (i : ι), IsOpen (U i)) (hU : s ⊆ ⋃ (i : ι), U i) : ∃ f, ((i : ι) → p ↑(↑f i)) ∧ BumpCovering.IsSubordinate f U

If X is a paracompact normal topological space and U is an open covering of a closed set s, then there exists a BumpCovering ι X s that is subordinate to U. This version assumes that p : (X → ℝ) → Prop is a predicate that satisfies Urysohn's lemma, and provides a BumpCovering such that each function of the covering satisfies p.

theorem BumpCovering.exists_isSubordinate {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} [NormalSpace X] [ParacompactSpace X] (hs : IsClosed s) (U : ι → Set X) (ho : ∀ (i : ι), IsOpen (U i)) (hU : s ⊆ ⋃ (i : ι), U i) : ∃ f, BumpCovering.IsSubordinate f U

If X is a paracompact normal topological space and U is an open covering of a closed set s, then there exists a BumpCovering ι X s that is subordinate to U.

def BumpCovering.ind {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (x : X) (hx : x ∈ s) : ι

Index of a bump function such that fs i =ᶠ[𝓝 x] 1.

theorem BumpCovering.eventuallyEq_one {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (x : X) (hx : x ∈ s) : ↑(↑f (BumpCovering.ind f x hx)) =ᶠ[nhds x] 1

theorem BumpCovering.ind_apply {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (x : X) (hx : x ∈ s) : ↑(↑f (BumpCovering.ind f x hx)) x = 1

def BumpCovering.toPOUFun {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) (x : X) : ℝ

Partition of unity defined by a BumpCovering. We use this auxiliary definition to prove some properties of the new family of functions before bundling it into a PartitionOfUnity. Do not use this definition, use BumpCovering.toPartitionOfUnity instead.

The partition of unity is given by the formula g i x = f i x * ∏ᶠ j < i, (1 - f j x). In other words, g i x = ∏ᶠ j < i, (1 - f j x) - ∏ᶠ j ≤ i, (1 - f j x), so ∑ᶠ i, g i x = 1 - ∏ᶠ j, (1 - f j x). If x ∈ s, then one of f j x equals one, hence the product of 1 - f j x vanishes, and ∑ᶠ i, g i x = 1.

In order to avoid an assumption LinearOrder ι, we use WellOrderingRel instead of (<).

theorem BumpCovering.toPOUFun_zero_of_zero {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) {i : ι} {x : X} (h : ↑(↑f i) x = 0) : BumpCovering.toPOUFun f i x = 0

theorem BumpCovering.support_toPOUFun_subset {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) : Function.support (BumpCovering.toPOUFun f i) ⊆ Function.support ↑(↑f i)

theorem BumpCovering.toPOUFun_eq_mul_prod {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) (x : X) (t : Finset ι) (ht : ∀ (j : ι), WellOrderingRel j i → ↑(↑f j) x ≠ 0 → j ∈ t) : BumpCovering.toPOUFun f i x = ↑(↑f i) x * Finset.prod (Finset.filter (fun j => WellOrderingRel j i) t) fun j => 1 - ↑(↑f j) x

theorem BumpCovering.sum_toPOUFun_eq {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (x : X) : ∑ᶠ (i : ι), BumpCovering.toPOUFun f i x = 1 - ∏ᶠ (i : ι), (1 - ↑(↑f i) x)

theorem BumpCovering.exists_finset_toPOUFun_eventuallyEq {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) (x : X) : ∃ t, BumpCovering.toPOUFun f i =ᶠ[nhds x] ↑(↑f i) * ↑(Finset.prod (Finset.filter (fun j => WellOrderingRel j i) t) fun j => 1 - ↑f j)

theorem BumpCovering.continuous_toPOUFun {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) : Continuous (BumpCovering.toPOUFun f i)

def BumpCovering.toPartitionOfUnity {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) : PartitionOfUnity ι X s

The partition of unity defined by a BumpCovering.

The partition of unity is given by the formula g i x = f i x * ∏ᶠ j < i, (1 - f j x). In other words, g i x = ∏ᶠ j < i, (1 - f j x) - ∏ᶠ j ≤ i, (1 - f j x), so ∑ᶠ i, g i x = 1 - ∏ᶠ j, (1 - f j x). If x ∈ s, then one of f j x equals one, hence the product of 1 - f j x vanishes, and ∑ᶠ i, g i x = 1.

In order to avoid an assumption LinearOrder ι, we use WellOrderingRel instead of (<).

theorem BumpCovering.toPartitionOfUnity_apply {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) (x : X) : ↑(↑(BumpCovering.toPartitionOfUnity f) i) x = ↑(↑f i) x * ∏ᶠ (j : ι) (_ : WellOrderingRel j i), (1 - ↑(↑f j) x)

theorem BumpCovering.toPartitionOfUnity_eq_mul_prod {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) (x : X) (t : Finset ι) (ht : ∀ (j : ι), WellOrderingRel j i → ↑(↑f j) x ≠ 0 → j ∈ t) : ↑(↑(BumpCovering.toPartitionOfUnity f) i) x = ↑(↑f i) x * Finset.prod (Finset.filter (fun j => WellOrderingRel j i) t) fun j => 1 - ↑(↑f j) x

theorem BumpCovering.exists_finset_toPartitionOfUnity_eventuallyEq {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) (x : X) : ∃ t, ↑(↑(BumpCovering.toPartitionOfUnity f) i) =ᶠ[nhds x] ↑(↑f i) * ↑(Finset.prod (Finset.filter (fun j => WellOrderingRel j i) t) fun j => 1 - ↑f j)

theorem BumpCovering.toPartitionOfUnity_zero_of_zero {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) {i : ι} {x : X} (h : ↑(↑f i) x = 0) : ↑(↑(BumpCovering.toPartitionOfUnity f) i) x = 0

theorem BumpCovering.support_toPartitionOfUnity_subset {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) : Function.support ↑(↑(BumpCovering.toPartitionOfUnity f) i) ⊆ Function.support ↑(↑f i)

theorem BumpCovering.sum_toPartitionOfUnity_eq {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (x : X) : ∑ᶠ (i : ι), ↑(↑(BumpCovering.toPartitionOfUnity f) i) x = 1 - ∏ᶠ (i : ι), (1 - ↑(↑f i) x)

theorem BumpCovering.IsSubordinate.toPartitionOfUnity {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} {f : BumpCovering ι X s} {U : ι → Set X} (h : BumpCovering.IsSubordinate f U) : PartitionOfUnity.IsSubordinate (BumpCovering.toPartitionOfUnity f) U

instance PartitionOfUnity.instInhabitedPartitionOfUnity {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} [Inhabited ι] : Inhabited (PartitionOfUnity ι X s)

theorem PartitionOfUnity.exists_isSubordinate_of_locallyFinite {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} [NormalSpace X] (hs : IsClosed s) (U : ι → Set X) (ho : ∀ (i : ι), IsOpen (U i)) (hf : LocallyFinite U) (hU : s ⊆ ⋃ (i : ι), U i) : ∃ f, PartitionOfUnity.IsSubordinate f U

If X is a normal topological space and U is a locally finite open covering of a closed set s, then there exists a PartitionOfUnity ι X s that is subordinate to U. If X is a paracompact space, then the assumption hf : LocallyFinite U can be omitted, see BumpCovering.exists_isSubordinate.

theorem PartitionOfUnity.exists_isSubordinate {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} [NormalSpace X] [ParacompactSpace X] (hs : IsClosed s) (U : ι → Set X) (ho : ∀ (i : ι), IsOpen (U i)) (hU : s ⊆ ⋃ (i : ι), U i) : ∃ f, PartitionOfUnity.IsSubordinate f U

If X is a paracompact normal topological space and U is an open covering of a closed set s, then there exists a PartitionOfUnity ι X s that is subordinate to U.