Commit 2022-07-04 19:58 8f391f56
View on Github →feat(geometry/euclidean/basic): continuous_at_angle (#15021)
Add lemmas that (unoriented) angles are continuous, as a function of a
pair of vectors or a triple of points, except where one of the vectors
is zero or one of the end points equals the middle point.