A convex set is contractible #
In this file we prove that a (star) convex set in a real topological vector space is a contractible topological space.
theorem
StarConvex.contractibleSpace
{E : Type u_1}
[AddCommGroup E]
[Module ℝ E]
[TopologicalSpace E]
[ContinuousAdd E]
[ContinuousSMul ℝ E]
{s : Set E}
{x : E}
(h : StarConvex ℝ x s)
(hne : Set.Nonempty s)
:
A non-empty star convex set is a contractible space.
theorem
Convex.contractibleSpace
{E : Type u_1}
[AddCommGroup E]
[Module ℝ E]
[TopologicalSpace E]
[ContinuousAdd E]
[ContinuousSMul ℝ E]
{s : Set E}
(hs : Convex ℝ s)
(hne : Set.Nonempty s)
:
A non-empty convex set is a contractible space.
instance
RealTopologicalVectorSpace.contractibleSpace
{E : Type u_1}
[AddCommGroup E]
[Module ℝ E]
[TopologicalSpace E]
[ContinuousAdd E]
[ContinuousSMul ℝ E]
:
Equations
- ⋯ = ⋯