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} [inst : TopologicalSpace X] [inst_1 : AddCommGroup E] [inst_2 : Module โ E]
[inst_3 : NormalSpace X] [inst_4 : ParacompactSpace X] [inst_5 : TopologicalSpace E] [inst_6 : ContinuousAdd E]
[inst_7 : ContinuousSMul โ E] {t : X โ Set E},
(โ (x : X), Convex โ (t x)) โ (โ (x : X), โ c, โแถ (y : X) in nhds x, c โ t y) โ โ g, โ (x : X), g x โ t x
The theorem `exists_continuous_forall_mem_convex_of_local_const` states that given a normal paracompact topological space `X` (for instance, an extended metric space) and a topological real vector space `E`, if we have a family `t` of convex sets indexed by `X` such that for each point `x` in `X`, there exists a vector `c` in `E` that lies in the set `t y` for all `y` in a neighborhood of `x`, then there exists a continuous function `g` from `X` to `E` such that the image of each point under `g` lies in the corresponding set in the family `t`. This theorem is related to the local constancy of a function and the property of convex sets.
More concisely: Given a normal paracompact topological space X and a topological real vector space E, if for each x in X there exists a vector c in E that lies in the convex set t(y) for all y in a neighborhood of x, then there exists a continuous function g from X to E such that g(x) โ t(x) for all x in X.
|
exists_continuous_forall_mem_convex_of_local
theorem exists_continuous_forall_mem_convex_of_local :
โ {X : Type u_2} {E : Type u_3} [inst : TopologicalSpace X] [inst_1 : AddCommGroup E] [inst_2 : Module โ E]
[inst_3 : NormalSpace X] [inst_4 : ParacompactSpace X] [inst_5 : TopologicalSpace E] [inst_6 : ContinuousAdd E]
[inst_7 : ContinuousSMul โ E] {t : X โ Set E},
(โ (x : X), Convex โ (t x)) โ
(โ (x : X), โ U โ nhds x, โ g, ContinuousOn g U โง โ y โ U, g y โ t y) โ โ g, โ (x : X), g x โ t x
The theorem `exists_continuous_forall_mem_convex_of_local` states the following:
Suppose `X` is a normal paracompact topological space (for example, any extended metric space), and `E` is a topological real vector space. Let `t` represent a family of convex sets, where each set is mapped from a point `x` in `X` to a set in `E`. If for every point `x` in `X`, there exists a neighborhood `U` in the neighborhood filter of `x` and a function `g` such that `g` is continuous on `U` and maps every point `y` in `U` to a point in `t y`, then there exists a continuous map `g` such that for every `x` in `X`, `g(x)` is an element of `t x`. This is a further condition of the theorem `exists_continuous_forall_mem_convex_of_local_const`.
More concisely: If for each point in a normal paracompact topological space `X` and every convex set family `t`, there exists a continuous function on a neighborhood of that point mapping to `t`, then there exists a continuous function mapping each point in `X` to an element in the corresponding `t` set.
|