Theorems · Theorem · general topology

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

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.

Defined in

Mathlib.Analysis.Convex.PartitionOfUnity

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceAddCommGroupModuleNormalSpaceParacompactSpaceTopologicalSpaceContinuousAddContinuousSMul