mathlib3 documentation

analysis.convex.partition_of_unity

Partition of unity and convex sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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} [topological_space X] [add_comm_group E] [module E] {s : set X} (f : partition_of_unity ι X s) {g : ι X E} {t : set E} {x : X} (hx : x s) (hg : (i : ι), (f i) x 0 g i x t) (ht : convex 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} [topological_space X] [add_comm_group E] [module E] [normal_space X] [paracompact_space X] [topological_space E] [has_continuous_add E] [has_continuous_smul E] {t : X set E} (ht : (x : X), convex (t x)) (H : (x : X), (U : set X) (H : U nhds x) (g : X E), continuous_on g U (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} [topological_space X] [add_comm_group E] [module E] [normal_space X] [paracompact_space X] [topological_space E] [has_continuous_add E] [has_continuous_smul E] {t : X set E} (ht : (x : X), convex (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.