Theorems · Theorem · general topology

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]
  [NormalSpace X] [ParacompactSpace X] [inst_5 : TopologicalSpace E] [ContinuousAdd E] [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

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.

Defined in

Mathlib.Analysis.Convex.PartitionOfUnity

Cited by

1 results in Mathlib

Foundations

Depth 171 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceAddCommGroupModuleNormalSpaceParacompactSpaceTopologicalSpaceContinuousAddContinuousSMul