mathlib3 documentation

analysis.convex.contractible

A convex set is contractible #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.