mathlib

e3f47f2b - feat(geometry/euclidean/oriented_angle): `continuous_at_oangle` (#15463)

feat(geometry/euclidean/oriented_angle): `continuous_at_oangle` (#15463) Add lemmas that oriented angles are continuous, as a function of a pair of vectors, except where one of the vectors is zero, analogous to the lemmas previously added for unoriented angles.