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 : s.Nonempty) : ContractibleSpace ↑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 : s.Nonempty) : ContractibleSpace ↑s

A non-empty convex set is a contractible space.

@[instance 100]

instance RealTopologicalVectorSpace.contractibleSpace {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] : ContractibleSpace E

Equations

• ⋯ = ⋯