The type of angles #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
In this file we define
real.angle to be the quotient group
ℝ/2πℤ and prove a few simple lemmas
about trigonometric functions and angles.
The type of angles
ℝ → angle as an additive homomorphism.
An induction principle to deduce results for
angle from those for
ℝ, used with
induction θ using real.angle.induction_on.
real.angle to a real number in the interval
Ioc (-π) π.
The sign of a
0 if the angle is
1 if the angle is strictly
-1 is the angle is strictly between
0. It is defined as the
sign of the sine of the angle.
Suppose a function to angles is continuous on a connected set and never takes the values
π on that set. Then the values of the function on that set all have the same sign.