# mathlibdocumentation

analysis.convex.partition_of_unity

# Partition of unity and convex sets #

In this file we prove the following lemma, see exists_continuous_forall_mem_convex_of_local. Let X be a normal paracompact topological space (e.g., any extended metric space). Let E be a topological real vector space. Let t : X β set E be a family of convex sets. Suppose that for each point x : X, there exists a neighborhood U β π X and a function g : X β E that is continuous on U and sends each y β U to a point of t y. Then there exists a continuous map g : C(X, E) such that g x β t x for all x.

We also formulate a useful corollary, see exists_continuous_forall_mem_convex_of_local_const, that assumes that local functions g are constants.

## Tags #

partition of unity

theorem partition_of_unity.finsum_smul_mem_convex {ΞΉ : Type u_1} {X : Type u_2} {E : Type u_3} [ E] {s : set X} (f : s) {g : ΞΉ β X β E} {t : set E} {x : X} (hx : x β s) (hg : β (i : ΞΉ), β(βf i) x β  0 β g i x β t) (ht : t) :
finsum (Ξ» (i : ΞΉ), β(βf i) x β’ g i x) β t
theorem exists_continuous_forall_mem_convex_of_local {X : Type u_2} {E : Type u_3} [ E] [normal_space X] {t : X β set E} (ht : β (x : X), (t x)) (H : β (x : X), β (U : set X) (H : U β nhds x) (g : X β E), β§ β (y : X), y β U β g y β t y) :
β (g : C(X, E)), β (x : X), βg x β t x

Let X be a normal paracompact topological space (e.g., any extended metric space). Let E be a topological real vector space. Let t : X β set E be a family of convex sets. Suppose that for each point x : X, there exists a neighborhood U β π X and a function g : X β E that is continuous on U and sends each y β U to a point of t y. Then there exists a continuous map g : C(X, E) such that g x β t x for all x. See also exists_continuous_forall_mem_convex_of_local_const.

theorem exists_continuous_forall_mem_convex_of_local_const {X : Type u_2} {E : Type u_3} [ E] [normal_space X] {t : X β set E} (ht : β (x : X), (t x)) (H : β (x : X), β (c : E), βαΆ  (y : X) in nhds x, c β t y) :
β (g : C(X, E)), β (x : X), βg x β t x

Let X be a normal paracompact topological space (e.g., any extended metric space). Let E be a topological real vector space. Let t : X β set E be a family of convex sets. Suppose that for each point x : X, there exists a vector c : E that belongs to t y for all y in a neighborhood of x. Then there exists a continuous map g : C(X, E) such that g x β t x for all x. See also exists_continuous_forall_mem_convex_of_local.