mathlib
8f391f56 - feat(geometry/euclidean/basic): `continuous_at_angle` (#15021)

Commit
3 years ago
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.
Author
Parents
Loading