feat(analysis/convex/between): betweenness and midpoints (#17412)
feat(analysis/convex/between): betweenness and midpoints (#17412)

Add two lemmas that the midpoint of two points is between those points.







leanprover-community/mathlib,leanprover-community/mathlib