oriented_angle): oriented angles and betweenness (#16824)

Commit

3 years ago

feat(geometry/euclidean/oriented_angle): oriented angles and betweenness (#16824) Add lemmas relating oriented angles to strict and weak betweenness of points.

Author

jsm28

Parents

abed0373

mathlib3 34c70db6 - feat(geometry/euclidean/oriented_angle): oriented angles and betweenness (#16824)

mathlib3
34c70db6 - feat(geometry/euclidean/oriented_angle): oriented angles and betweenness (#16824)