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]
theorem
star_convex.contractible_space
{E : Type u_1}
[add_comm_group E]
[module ℝ E]
[topological_space E]
[has_continuous_add E]
[has_continuous_smul ℝ E]
{s : set E}
{x : E}
(h : star_convex ℝ x s)
(hne : s.nonempty) :
A non-empty star convex set is a contractible space.
@[protected]
theorem
convex.contractible_space
{E : Type u_1}
[add_comm_group E]
[module ℝ E]
[topological_space E]
[has_continuous_add E]
[has_continuous_smul ℝ E]
{s : set E}
(hs : convex ℝ s)
(hne : s.nonempty) :
A non-empty convex set is a contractible space.
@[protected, instance]
def
real_topological_vector_space.contractible_space
{E : Type u_1}
[add_comm_group E]
[module ℝ E]
[topological_space E]
[has_continuous_add E]
[has_continuous_smul ℝ E] :