mathlib documentation

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.

@[protected]

A non-empty star convex set is a contractible space.

@[protected]

A non-empty convex set is a contractible space.