Documentation

Mathlib.Analysis.Convex.PartitionOfUnity

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 PartitionOfUnity.finsum_smul_mem_convex {ฮน : Type u_1} {X : Type u_2} {E : Type u_3} [TopologicalSpace X] [AddCommGroup E] [Module โ„ E] {s : Set X} (f : PartitionOfUnity ฮน 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) :
โˆ‘แถ  (i : ฮน), (f i) x โ€ข g i x โˆˆ t
theorem exists_continuous_forall_mem_convex_of_local {X : Type u_2} {E : Type u_3} [TopologicalSpace X] [AddCommGroup E] [Module โ„ E] [NormalSpace X] [ParacompactSpace X] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul โ„ E] {t : X โ†’ Set E} (ht : โˆ€ (x : X), Convex โ„ (t x)) (H : โˆ€ (x : X), โˆƒ U โˆˆ nhds x, โˆƒ (g : X โ†’ E), ContinuousOn g U โˆง โˆ€ 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} [TopologicalSpace X] [AddCommGroup E] [Module โ„ E] [NormalSpace X] [ParacompactSpace X] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul โ„ 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.