Documentation

Mathlib.Analysis.Convex.Contractible

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) :

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) :

A non-empty convex set is a contractible space.