Documentation

Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

The type of angles #

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

Equations
Instances For

    The canonical map from to the quotient Angle.

    Equations
    • r = r
    Instances For

      Coercion ℝ → Angle as an additive homomorphism.

      Equations
      Instances For
        theorem Real.Angle.induction_on {p : Real.AngleProp} (θ : Real.Angle) (h : (x : ) → p x) :
        p θ

        An induction principle to deduce results for Angle from those for , used with induction θ using Real.Angle.induction_on.

        @[simp]
        theorem Real.Angle.coe_zero :
        0 = 0
        @[simp]
        theorem Real.Angle.coe_add (x : ) (y : ) :
        ↑(x + y) = x + y
        @[simp]
        theorem Real.Angle.coe_neg (x : ) :
        ↑(-x) = -x
        @[simp]
        theorem Real.Angle.coe_sub (x : ) (y : ) :
        ↑(x - y) = x - y
        theorem Real.Angle.coe_nsmul (n : ) (x : ) :
        ↑(n x) = n x
        theorem Real.Angle.coe_zsmul (z : ) (x : ) :
        ↑(z x) = z x
        @[simp]
        theorem Real.Angle.coe_nat_mul_eq_nsmul (x : ) (n : ) :
        ↑(n * x) = n x
        @[simp]
        theorem Real.Angle.coe_int_mul_eq_zsmul (x : ) (n : ) :
        ↑(n * x) = n x
        theorem Real.Angle.angle_eq_iff_two_pi_dvd_sub {ψ : } {θ : } :
        θ = ψ k, θ - ψ = 2 * Real.pi * k
        @[simp]
        theorem Real.Angle.coe_two_pi :
        ↑(2 * Real.pi) = 0
        @[simp]
        theorem Real.Angle.two_nsmul_coe_div_two (θ : ) :
        2 ↑(θ / 2) = θ
        @[simp]
        theorem Real.Angle.two_zsmul_coe_div_two (θ : ) :
        2 ↑(θ / 2) = θ
        theorem Real.Angle.zsmul_eq_iff {ψ : Real.Angle} {θ : Real.Angle} {z : } (hz : z 0) :
        z ψ = z θ k, ψ = θ + ↑(k (2 * Real.pi / z))
        theorem Real.Angle.nsmul_eq_iff {ψ : Real.Angle} {θ : Real.Angle} {n : } (hz : n 0) :
        n ψ = n θ k, ψ = θ + ↑(k (2 * Real.pi / n))
        theorem Real.Angle.two_zsmul_eq_iff {ψ : Real.Angle} {θ : Real.Angle} :
        2 ψ = 2 θ ψ = θ ψ = θ + Real.pi
        theorem Real.Angle.two_nsmul_eq_iff {ψ : Real.Angle} {θ : Real.Angle} :
        2 ψ = 2 θ ψ = θ ψ = θ + Real.pi
        theorem Real.Angle.eq_neg_self_iff {θ : Real.Angle} :
        θ = -θ θ = 0 θ = Real.pi
        theorem Real.Angle.neg_eq_self_iff {θ : Real.Angle} :
        -θ = θ θ = 0 θ = Real.pi
        theorem Real.Angle.two_nsmul_eq_pi_iff {θ : Real.Angle} :
        2 θ = Real.pi θ = ↑(Real.pi / 2) θ = ↑(-Real.pi / 2)
        theorem Real.Angle.two_zsmul_eq_pi_iff {θ : Real.Angle} :
        2 θ = Real.pi θ = ↑(Real.pi / 2) θ = ↑(-Real.pi / 2)
        theorem Real.Angle.cos_eq_iff_coe_eq_or_eq_neg {θ : } {ψ : } :
        Real.cos θ = Real.cos ψ θ = ψ θ = -ψ
        theorem Real.Angle.sin_eq_iff_coe_eq_or_add_eq_pi {θ : } {ψ : } :
        Real.sin θ = Real.sin ψ θ = ψ θ + ψ = Real.pi
        theorem Real.Angle.cos_sin_inj {θ : } {ψ : } (Hcos : Real.cos θ = Real.cos ψ) (Hsin : Real.sin θ = Real.sin ψ) :
        θ = ψ
        @[simp]
        @[simp]
        @[simp]
        theorem Real.Angle.coe_toIcoMod (θ : ) (ψ : ) :
        ↑(toIcoMod Real.two_pi_pos ψ θ) = θ
        @[simp]
        theorem Real.Angle.coe_toIocMod (θ : ) (ψ : ) :
        ↑(toIocMod Real.two_pi_pos ψ θ) = θ

        Convert a Real.Angle to a real number in the interval Ioc (-π) π.

        Equations
        Instances For
          @[simp]
          theorem Real.Angle.toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff {θ : } {k : } :
          Real.Angle.toReal θ = θ - 2 * k * Real.pi θ Set.Ioc ((2 * k - 1) * Real.pi) ((2 * k + 1) * Real.pi)

          The tangent of a Real.Angle.

          Equations
          Instances For
            @[simp]

            The sign of a Real.Angle is 0 if the angle is 0 or π, 1 if the angle is strictly between 0 and π and -1 is the angle is strictly between and 0. It is defined as the sign of the sine of the angle.

            Equations
            Instances For
              @[simp]
              theorem Real.Angle.sign_toReal {θ : Real.Angle} (h : θ Real.pi) :
              SignType.sign (Real.Angle.toReal θ) = Real.Angle.sign θ
              theorem ContinuousOn.angle_sign_comp {α : Type u_1} [TopologicalSpace α] {f : αReal.Angle} {s : Set α} (hf : ContinuousOn f s) (hs : ∀ (z : α), z sf z 0 f z Real.pi) :
              theorem Real.Angle.sign_eq_of_continuousOn {α : Type u_1} [TopologicalSpace α] {f : αReal.Angle} {s : Set α} {x : α} {y : α} (hc : IsConnected s) (hf : ContinuousOn f s) (hs : ∀ (z : α), z sf z 0 f z Real.pi) (hx : x s) (hy : y s) :

              Suppose a function to angles is continuous on a connected set and never takes the values 0 or π on that set. Then the values of the function on that set all have the same sign.