feat: port Analysis.Convex.Between (#3790)

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: ADedecker <anatolededecker@gmail.com> Co-authored-by: Alex J Best <alex.j.best@gmail.com>
leanprover-community · May 22, 2023 · 9247bc4 · 9247bc4
1 parent c59c263
commit 9247bc4
Show file tree

Hide file tree

Showing 3 changed files with 929 additions and 1 deletion.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -385,6 +385,7 @@ import Mathlib.Analysis.Complex.Circle
 import Mathlib.Analysis.Complex.OperatorNorm
 import Mathlib.Analysis.Complex.ReImTopology
 import Mathlib.Analysis.Convex.Basic
+import Mathlib.Analysis.Convex.Between
 import Mathlib.Analysis.Convex.Body
 import Mathlib.Analysis.Convex.Caratheodory
 import Mathlib.Analysis.Convex.Combination