Michael's selection theorem #
This file proves Michael's selection theorem, that a lower hemicontinuous function with convex closed nonempty values admits a continuous selection.
Main results #
HasOpenLowerSections.exists_continuous_selection: A correspondence with open lower sections and convex, nonempty values admits a continuous selection. A key ingredient to the proof of Michael's selection theorem. This holds in any topological vector space over ℝ.LowerHemicontinuous.exists_continuous_selection: Michael's selection theorem that a lower hemicontinuous function from a paracompact space to a Fréchet space which takes convex, closed, nonempty values admits a continuous selection.
theorem
LowerHemicontinuous.hasOpenCGraph_of_add_hasOpenCGraph
{α : Type u_1}
{β : Type u_2}
{f : α → Set β}
[TopologicalSpace α]
[TopologicalSpace β]
[AddGroup β]
[IsTopologicalAddGroup β]
{g : α → Set β}
(hf : LowerHemicontinuous f)
(hg : HasOpenCGraph g)
:
HasOpenCGraph (f + g)
theorem
HasOpenLowerSections.exists_continuous_selection
{α : Type u_1}
{β : Type u_2}
{f : α → Set β}
[TopologicalSpace α]
[NormalSpace α]
[ParacompactSpace α]
[AddCommGroup β]
[Module ℝ β]
[TopologicalSpace β]
[ContinuousSMul ℝ β]
[ContinuousAdd β]
(hf : HasOpenLowerSections f)
(hf_nonempty : ∀ (x : α), (f x).Nonempty)
(hf_convex : ∀ (x : α), Convex ℝ (f x))
:
∃ (h : α → β), Continuous h ∧ ∀ (x : α), h x ∈ f x
Michael's selection theorem (approximate): A correspondence with open lower sections and
convex, nonempty values admits a continuous selection. This holds in any topological vector space
over ℝ.
theorem
LowerHemicontinuous.exists_continuous_selection
{α : Type u_1}
{β : Type u_2}
{f : α → Set β}
[TopologicalSpace α]
[NormalSpace α]
[ParacompactSpace α]
[AddCommGroup β]
[Module ℝ β]
[UniformSpace β]
[IsUniformAddGroup β]
[ContinuousSMul ℝ β]
[LocallyConvexSpace ℝ β]
[FirstCountableTopology β]
[CompleteSpace β]
(hf : LowerHemicontinuous f)
(hf_nonempty : ∀ (x : α), (f x).Nonempty)
(hf_convex : ∀ (x : α), Convex ℝ (f x))
(hf_isClosed : ∀ (x : α), IsClosed (f x))
:
∃ (g : α → β), Continuous g ∧ ∀ (x : α), g x ∈ f x
Michael's selection theorem: A lower hemicontinuous function from a paracompact normal space to a Fréchet space with nonempty convex closed values admits a continuous selection