side): betweenness and `point_reflection` (#16937)

Commit

3 years ago

feat(analysis/convex/between,analysis/convex/side): betweenness and `point_reflection` (#16937) Add lemmas about betweenness properties involving `point_reflection`.

Author

jsm28

Parents

f45d3379

mathlib3 8b7c3f5b - feat(analysis/convex/between,analysis/convex/side): betweenness and `point_reflection` (#16937)

mathlib3
8b7c3f5b - feat(analysis/convex/between,analysis/convex/side): betweenness and `point_reflection` (#16937)