mathlib3

40427f78 - feat(analysis/special_functions/trigonometric/angle): continuity and signs (#16204)

feat(analysis/special_functions/trigonometric/angle): continuity and signs (#16204) Add the lemmas that `real.angle.sign` is continuous away from 0 and π, and thus that any function to angles that is continuous on a connected set and does not take the value 0 or π on that set produces angles with constant sign on that set (this is a general principle for use in proving results about when two oriented angles in a geometrical configuration must have the same sign).