feat: port Analysis.Convex.Contractible (#3983)

Mathlib.lean

@@ -358,6 +358,7 @@ import Mathlib.Analysis.Convex.Body
 import Mathlib.Analysis.Convex.Caratheodory
 import Mathlib.Analysis.Convex.Combination
 import Mathlib.Analysis.Convex.Complex
+import Mathlib.Analysis.Convex.Contractible
 import Mathlib.Analysis.Convex.Exposed
 import Mathlib.Analysis.Convex.Extrema
 import Mathlib.Analysis.Convex.Extreme

Mathlib/Analysis/Convex/Contractible.lean

@@ -0,0 +1,54 @@
+/-
+Copyright (c) 2022 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+
+! This file was ported from Lean 3 source module analysis.convex.contractible
+! leanprover-community/mathlib commit 3339976e2bcae9f1c81e620836d1eb736e3c4700
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Analysis.Convex.Star
+import Mathlib.Topology.Homotopy.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.
+-/
+
+
+variable {E : Type _} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E]
+  [ContinuousSMul ℝ E] {s : Set E} {x : E}
+
+/-- A non-empty star convex set is a contractible space. -/
+protected theorem StarConvex.contractibleSpace (h : StarConvex ℝ x s) (hne : s.Nonempty) :
+    ContractibleSpace s := by
+  refine'
+    (contractible_iff_id_nullhomotopic s).2
+      ⟨⟨x, h.mem hne⟩,
+        ⟨⟨⟨fun p => ⟨p.1.1 • x + (1 - p.1.1) • (p.2 : E), _⟩, _⟩, fun x => _, fun x => _⟩⟩⟩
+  · exact h p.2.2 p.1.2.1 (sub_nonneg.2 p.1.2.2) (add_sub_cancel'_right _ _)
+  · exact
+      ((continuous_subtype_val.fst'.smul continuous_const).add
+            ((continuous_const.sub continuous_subtype_val.fst').smul
+              continuous_subtype_val.snd')).subtype_mk
+        _
+  · ext1
+    simp
+  · ext1
+    simp
+#align star_convex.contractible_space StarConvex.contractibleSpace
+
+/-- A non-empty convex set is a contractible space. -/
+protected theorem Convex.contractibleSpace (hs : Convex ℝ s) (hne : s.Nonempty) :
+    ContractibleSpace s :=
+  let ⟨_, hx⟩ := hne
+  (hs.starConvex hx).contractibleSpace hne
+#align convex.contractible_space Convex.contractibleSpace
+
+instance (priority := 100) RealTopologicalVectorSpace.contractibleSpace : ContractibleSpace E :=
+  (Homeomorph.Set.univ E).contractibleSpace_iff.mp <|
+    convex_univ.contractibleSpace Set.univ_nonempty
+#align real_topological_vector_space.contractible_space RealTopologicalVectorSpace.contractibleSpace