Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-18 08:07 e3f47f2b

View on Github →

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.

Estimated changes