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.

def Real.Angle : Type

The type of angles

instance Real.Angle.instNormedAddCommGroupAngle : NormedAddCommGroup Real.Angle

instance Real.Angle.instInhabitedAngle : Inhabited Real.Angle

def Real.Angle.coe (r : ℝ) : Real.Angle

The canonical map from ℝ to the quotient Angle.

instance Real.Angle.instCoeRealAngle : Coe ℝ Real.Angle

instance Real.Angle.instCircularOrderAngle : CircularOrder Real.Angle

theorem Real.Angle.continuous_coe : Continuous Real.Angle.coe

def Real.Angle.coeHom : ℝ →+ Real.Angle

Coercion ℝ → Angle as an additive homomorphism.

@[simp]

theorem Real.Angle.coe_coeHom : ↑Real.Angle.coeHom = Real.Angle.coe

theorem Real.Angle.induction_on {p : Real.Angle → Prop} (θ : 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.neg_coe_pi : -↑Real.pi = ↑Real.pi

@[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.two_nsmul_neg_pi_div_two : 2 • ↑(-Real.pi / 2) = ↑Real.pi

theorem Real.Angle.two_zsmul_neg_pi_div_two : 2 • ↑(-Real.pi / 2) = ↑Real.pi

theorem Real.Angle.sub_coe_pi_eq_add_coe_pi (θ : Real.Angle) : θ - ↑Real.pi = θ + ↑Real.pi

@[simp]

theorem Real.Angle.two_nsmul_coe_pi : 2 • ↑Real.pi = 0

@[simp]

theorem Real.Angle.two_zsmul_coe_pi : 2 • ↑Real.pi = 0

@[simp]

theorem Real.Angle.coe_pi_add_coe_pi : ↑Real.pi + ↑Real.pi = 0

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.two_nsmul_eq_zero_iff {θ : Real.Angle} : 2 • θ = 0 ↔ θ = 0 ∨ θ = ↑Real.pi

theorem Real.Angle.two_nsmul_ne_zero_iff {θ : Real.Angle} : 2 • θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑Real.pi

theorem Real.Angle.two_zsmul_eq_zero_iff {θ : Real.Angle} : 2 • θ = 0 ↔ θ = 0 ∨ θ = ↑Real.pi

theorem Real.Angle.two_zsmul_ne_zero_iff {θ : Real.Angle} : 2 • θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑Real.pi

theorem Real.Angle.eq_neg_self_iff {θ : Real.Angle} : θ = -θ ↔ θ = 0 ∨ θ = ↑Real.pi

theorem Real.Angle.ne_neg_self_iff {θ : Real.Angle} : θ ≠ -θ ↔ θ ≠ 0 ∧ θ ≠ ↑Real.pi

theorem Real.Angle.neg_eq_self_iff {θ : Real.Angle} : -θ = θ ↔ θ = 0 ∨ θ = ↑Real.pi

theorem Real.Angle.neg_ne_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 ψ) : ↑θ = ↑ψ

def Real.Angle.sin (θ : Real.Angle) : ℝ

The sine of a Real.Angle.

@[simp]

theorem Real.Angle.sin_coe (x : ℝ) : Real.Angle.sin ↑x = Real.sin x

theorem Real.Angle.continuous_sin : Continuous Real.Angle.sin

def Real.Angle.cos (θ : Real.Angle) : ℝ

The cosine of a Real.Angle.

@[simp]

theorem Real.Angle.cos_coe (x : ℝ) : Real.Angle.cos ↑x = Real.cos x

theorem Real.Angle.continuous_cos : Continuous Real.Angle.cos

theorem Real.Angle.cos_eq_real_cos_iff_eq_or_eq_neg {θ : Real.Angle} {ψ : ℝ} : Real.Angle.cos θ = Real.cos ψ ↔ θ = ↑ψ ∨ θ = -↑ψ

theorem Real.Angle.cos_eq_iff_eq_or_eq_neg {θ : Real.Angle} {ψ : Real.Angle} : Real.Angle.cos θ = Real.Angle.cos ψ ↔ θ = ψ ∨ θ = -ψ

theorem Real.Angle.sin_eq_real_sin_iff_eq_or_add_eq_pi {θ : Real.Angle} {ψ : ℝ} : Real.Angle.sin θ = Real.sin ψ ↔ θ = ↑ψ ∨ θ + ↑ψ = ↑Real.pi

theorem Real.Angle.sin_eq_iff_eq_or_add_eq_pi {θ : Real.Angle} {ψ : Real.Angle} : Real.Angle.sin θ = Real.Angle.sin ψ ↔ θ = ψ ∨ θ + ψ = ↑Real.pi

@[simp]

theorem Real.Angle.sin_zero : Real.Angle.sin 0 = 0

theorem Real.Angle.sin_coe_pi : Real.Angle.sin ↑Real.pi = 0

theorem Real.Angle.sin_eq_zero_iff {θ : Real.Angle} : Real.Angle.sin θ = 0 ↔ θ = 0 ∨ θ = ↑Real.pi

theorem Real.Angle.sin_ne_zero_iff {θ : Real.Angle} : Real.Angle.sin θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑Real.pi

@[simp]

theorem Real.Angle.sin_neg (θ : Real.Angle) : Real.Angle.sin (-θ) = -Real.Angle.sin θ

theorem Real.Angle.sin_antiperiodic : Function.Antiperiodic Real.Angle.sin ↑Real.pi

@[simp]

theorem Real.Angle.sin_add_pi (θ : Real.Angle) : Real.Angle.sin (θ + ↑Real.pi) = -Real.Angle.sin θ

@[simp]

theorem Real.Angle.sin_sub_pi (θ : Real.Angle) : Real.Angle.sin (θ - ↑Real.pi) = -Real.Angle.sin θ

@[simp]

theorem Real.Angle.cos_zero : Real.Angle.cos 0 = 1

theorem Real.Angle.cos_coe_pi : Real.Angle.cos ↑Real.pi = -1

@[simp]

theorem Real.Angle.cos_neg (θ : Real.Angle) : Real.Angle.cos (-θ) = Real.Angle.cos θ

theorem Real.Angle.cos_antiperiodic : Function.Antiperiodic Real.Angle.cos ↑Real.pi

@[simp]

theorem Real.Angle.cos_add_pi (θ : Real.Angle) : Real.Angle.cos (θ + ↑Real.pi) = -Real.Angle.cos θ

@[simp]

theorem Real.Angle.cos_sub_pi (θ : Real.Angle) : Real.Angle.cos (θ - ↑Real.pi) = -Real.Angle.cos θ

theorem Real.Angle.cos_eq_zero_iff {θ : Real.Angle} : Real.Angle.cos θ = 0 ↔ θ = ↑(Real.pi / 2) ∨ θ = ↑(-Real.pi / 2)

theorem Real.Angle.sin_add (θ₁ : Real.Angle) (θ₂ : Real.Angle) : Real.Angle.sin (θ₁ + θ₂) = Real.Angle.sin θ₁ * Real.Angle.cos θ₂ + Real.Angle.cos θ₁ * Real.Angle.sin θ₂

theorem Real.Angle.cos_add (θ₁ : Real.Angle) (θ₂ : Real.Angle) : Real.Angle.cos (θ₁ + θ₂) = Real.Angle.cos θ₁ * Real.Angle.cos θ₂ - Real.Angle.sin θ₁ * Real.Angle.sin θ₂

@[simp]

theorem Real.Angle.cos_sq_add_sin_sq (θ : Real.Angle) : Real.Angle.cos θ ^ 2 + Real.Angle.sin θ ^ 2 = 1

theorem Real.Angle.sin_add_pi_div_two (θ : Real.Angle) : Real.Angle.sin (θ + ↑(Real.pi / 2)) = Real.Angle.cos θ

theorem Real.Angle.sin_sub_pi_div_two (θ : Real.Angle) : Real.Angle.sin (θ - ↑(Real.pi / 2)) = -Real.Angle.cos θ

theorem Real.Angle.sin_pi_div_two_sub (θ : Real.Angle) : Real.Angle.sin (↑(Real.pi / 2) - θ) = Real.Angle.cos θ

theorem Real.Angle.cos_add_pi_div_two (θ : Real.Angle) : Real.Angle.cos (θ + ↑(Real.pi / 2)) = -Real.Angle.sin θ

theorem Real.Angle.cos_sub_pi_div_two (θ : Real.Angle) : Real.Angle.cos (θ - ↑(Real.pi / 2)) = Real.Angle.sin θ

theorem Real.Angle.cos_pi_div_two_sub (θ : Real.Angle) : Real.Angle.cos (↑(Real.pi / 2) - θ) = Real.Angle.sin θ

theorem Real.Angle.abs_sin_eq_of_two_nsmul_eq {θ : Real.Angle} {ψ : Real.Angle} (h : 2 • θ = 2 • ψ) : |Real.Angle.sin θ| = |Real.Angle.sin ψ|

theorem Real.Angle.abs_sin_eq_of_two_zsmul_eq {θ : Real.Angle} {ψ : Real.Angle} (h : 2 • θ = 2 • ψ) : |Real.Angle.sin θ| = |Real.Angle.sin ψ|

theorem Real.Angle.abs_cos_eq_of_two_nsmul_eq {θ : Real.Angle} {ψ : Real.Angle} (h : 2 • θ = 2 • ψ) : |Real.Angle.cos θ| = |Real.Angle.cos ψ|

theorem Real.Angle.abs_cos_eq_of_two_zsmul_eq {θ : Real.Angle} {ψ : Real.Angle} (h : 2 • θ = 2 • ψ) : |Real.Angle.cos θ| = |Real.Angle.cos ψ|

@[simp]

theorem Real.Angle.coe_toIcoMod (θ : ℝ) (ψ : ℝ) : ↑(toIcoMod Real.two_pi_pos ψ θ) = ↑θ

@[simp]

theorem Real.Angle.coe_toIocMod (θ : ℝ) (ψ : ℝ) : ↑(toIocMod Real.two_pi_pos ψ θ) = ↑θ

def Real.Angle.toReal (θ : Real.Angle) : ℝ

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

theorem Real.Angle.toReal_coe (θ : ℝ) : Real.Angle.toReal ↑θ = toIocMod Real.two_pi_pos (-Real.pi) θ

theorem Real.Angle.toReal_coe_eq_self_iff {θ : ℝ} : Real.Angle.toReal ↑θ = θ ↔ -Real.pi < θ ∧ θ ≤ Real.pi

theorem Real.Angle.toReal_coe_eq_self_iff_mem_Ioc {θ : ℝ} : Real.Angle.toReal ↑θ = θ ↔ θ ∈ Set.Ioc (-Real.pi) Real.pi

theorem Real.Angle.toReal_injective : Function.Injective Real.Angle.toReal

@[simp]

theorem Real.Angle.toReal_inj {θ : Real.Angle} {ψ : Real.Angle} : Real.Angle.toReal θ = Real.Angle.toReal ψ ↔ θ = ψ

@[simp]

theorem Real.Angle.coe_toReal (θ : Real.Angle) : ↑(Real.Angle.toReal θ) = θ

theorem Real.Angle.neg_pi_lt_toReal (θ : Real.Angle) : -Real.pi < Real.Angle.toReal θ

theorem Real.Angle.toReal_le_pi (θ : Real.Angle) : Real.Angle.toReal θ ≤ Real.pi

theorem Real.Angle.abs_toReal_le_pi (θ : Real.Angle) : |Real.Angle.toReal θ| ≤ Real.pi

theorem Real.Angle.toReal_mem_Ioc (θ : Real.Angle) : Real.Angle.toReal θ ∈ Set.Ioc (-Real.pi) Real.pi

@[simp]

theorem Real.Angle.toIocMod_toReal (θ : Real.Angle) : toIocMod Real.two_pi_pos (-Real.pi) (Real.Angle.toReal θ) = Real.Angle.toReal θ

@[simp]

theorem Real.Angle.toReal_zero : Real.Angle.toReal 0 = 0

@[simp]

theorem Real.Angle.toReal_eq_zero_iff {θ : Real.Angle} : Real.Angle.toReal θ = 0 ↔ θ = 0

@[simp]

theorem Real.Angle.toReal_pi : Real.Angle.toReal ↑Real.pi = Real.pi

@[simp]

theorem Real.Angle.toReal_eq_pi_iff {θ : Real.Angle} : Real.Angle.toReal θ = Real.pi ↔ θ = ↑Real.pi

theorem Real.Angle.pi_ne_zero : ↑Real.pi ≠ 0

@[simp]

theorem Real.Angle.toReal_pi_div_two : Real.Angle.toReal ↑(Real.pi / 2) = Real.pi / 2

@[simp]

theorem Real.Angle.toReal_eq_pi_div_two_iff {θ : Real.Angle} : Real.Angle.toReal θ = Real.pi / 2 ↔ θ = ↑(Real.pi / 2)

@[simp]

theorem Real.Angle.toReal_neg_pi_div_two : Real.Angle.toReal ↑(-Real.pi / 2) = -Real.pi / 2

@[simp]

theorem Real.Angle.toReal_eq_neg_pi_div_two_iff {θ : Real.Angle} : Real.Angle.toReal θ = -Real.pi / 2 ↔ θ = ↑(-Real.pi / 2)

theorem Real.Angle.pi_div_two_ne_zero : ↑(Real.pi / 2) ≠ 0

theorem Real.Angle.neg_pi_div_two_ne_zero : ↑(-Real.pi / 2) ≠ 0

theorem Real.Angle.abs_toReal_coe_eq_self_iff {θ : ℝ} : |Real.Angle.toReal ↑θ| = θ ↔ 0 ≤ θ ∧ θ ≤ Real.pi

theorem Real.Angle.abs_toReal_neg_coe_eq_self_iff {θ : ℝ} : |Real.Angle.toReal (-↑θ)| = θ ↔ 0 ≤ θ ∧ θ ≤ Real.pi

theorem Real.Angle.abs_toReal_eq_pi_div_two_iff {θ : Real.Angle} : |Real.Angle.toReal θ| = Real.pi / 2 ↔ θ = ↑(Real.pi / 2) ∨ θ = ↑(-Real.pi / 2)

theorem Real.Angle.nsmul_toReal_eq_mul {n : ℕ} (h : n ≠ 0) {θ : Real.Angle} : Real.Angle.toReal (n • θ) = ↑n * Real.Angle.toReal θ ↔ Real.Angle.toReal θ ∈ Set.Ioc (-Real.pi / ↑n) (Real.pi / ↑n)

theorem Real.Angle.two_nsmul_toReal_eq_two_mul {θ : Real.Angle} : Real.Angle.toReal (2 • θ) = 2 * Real.Angle.toReal θ ↔ Real.Angle.toReal θ ∈ Set.Ioc (-Real.pi / 2) (Real.pi / 2)

theorem Real.Angle.two_zsmul_toReal_eq_two_mul {θ : Real.Angle} : Real.Angle.toReal (2 • θ) = 2 * Real.Angle.toReal θ ↔ Real.Angle.toReal θ ∈ Set.Ioc (-Real.pi / 2) (Real.pi / 2)

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)

theorem Real.Angle.toReal_coe_eq_self_sub_two_pi_iff {θ : ℝ} : Real.Angle.toReal ↑θ = θ - 2 * Real.pi ↔ θ ∈ Set.Ioc Real.pi (3 * Real.pi)

theorem Real.Angle.toReal_coe_eq_self_add_two_pi_iff {θ : ℝ} : Real.Angle.toReal ↑θ = θ + 2 * Real.pi ↔ θ ∈ Set.Ioc (-3 * Real.pi) (-Real.pi)

theorem Real.Angle.two_nsmul_toReal_eq_two_mul_sub_two_pi {θ : Real.Angle} : Real.Angle.toReal (2 • θ) = 2 * Real.Angle.toReal θ - 2 * Real.pi ↔ Real.pi / 2 < Real.Angle.toReal θ

theorem Real.Angle.two_zsmul_toReal_eq_two_mul_sub_two_pi {θ : Real.Angle} : Real.Angle.toReal (2 • θ) = 2 * Real.Angle.toReal θ - 2 * Real.pi ↔ Real.pi / 2 < Real.Angle.toReal θ

theorem Real.Angle.two_nsmul_toReal_eq_two_mul_add_two_pi {θ : Real.Angle} : Real.Angle.toReal (2 • θ) = 2 * Real.Angle.toReal θ + 2 * Real.pi ↔ Real.Angle.toReal θ ≤ -Real.pi / 2

theorem Real.Angle.two_zsmul_toReal_eq_two_mul_add_two_pi {θ : Real.Angle} : Real.Angle.toReal (2 • θ) = 2 * Real.Angle.toReal θ + 2 * Real.pi ↔ Real.Angle.toReal θ ≤ -Real.pi / 2

@[simp]

theorem Real.Angle.sin_toReal (θ : Real.Angle) : Real.sin (Real.Angle.toReal θ) = Real.Angle.sin θ

@[simp]

theorem Real.Angle.cos_toReal (θ : Real.Angle) : Real.cos (Real.Angle.toReal θ) = Real.Angle.cos θ

theorem Real.Angle.cos_nonneg_iff_abs_toReal_le_pi_div_two {θ : Real.Angle} : 0 ≤ Real.Angle.cos θ ↔ |Real.Angle.toReal θ| ≤ Real.pi / 2

theorem Real.Angle.cos_pos_iff_abs_toReal_lt_pi_div_two {θ : Real.Angle} : 0 < Real.Angle.cos θ ↔ |Real.Angle.toReal θ| < Real.pi / 2

theorem Real.Angle.cos_neg_iff_pi_div_two_lt_abs_toReal {θ : Real.Angle} : Real.Angle.cos θ < 0 ↔ Real.pi / 2 < |Real.Angle.toReal θ|

theorem Real.Angle.abs_cos_eq_abs_sin_of_two_nsmul_add_two_nsmul_eq_pi {θ : Real.Angle} {ψ : Real.Angle} (h : 2 • θ + 2 • ψ = ↑Real.pi) : |Real.Angle.cos θ| = |Real.Angle.sin ψ|

theorem Real.Angle.abs_cos_eq_abs_sin_of_two_zsmul_add_two_zsmul_eq_pi {θ : Real.Angle} {ψ : Real.Angle} (h : 2 • θ + 2 • ψ = ↑Real.pi) : |Real.Angle.cos θ| = |Real.Angle.sin ψ|

def Real.Angle.tan (θ : Real.Angle) : ℝ

The tangent of a Real.Angle.

theorem Real.Angle.tan_eq_sin_div_cos (θ : Real.Angle) : Real.Angle.tan θ = Real.Angle.sin θ / Real.Angle.cos θ

@[simp]

theorem Real.Angle.tan_coe (x : ℝ) : Real.Angle.tan ↑x = Real.tan x

@[simp]

theorem Real.Angle.tan_zero : Real.Angle.tan 0 = 0

theorem Real.Angle.tan_coe_pi : Real.Angle.tan ↑Real.pi = 0

theorem Real.Angle.tan_periodic : Function.Periodic Real.Angle.tan ↑Real.pi

@[simp]

theorem Real.Angle.tan_add_pi (θ : Real.Angle) : Real.Angle.tan (θ + ↑Real.pi) = Real.Angle.tan θ

@[simp]

theorem Real.Angle.tan_sub_pi (θ : Real.Angle) : Real.Angle.tan (θ - ↑Real.pi) = Real.Angle.tan θ

@[simp]

theorem Real.Angle.tan_toReal (θ : Real.Angle) : Real.tan (Real.Angle.toReal θ) = Real.Angle.tan θ

theorem Real.Angle.tan_eq_of_two_nsmul_eq {θ : Real.Angle} {ψ : Real.Angle} (h : 2 • θ = 2 • ψ) : Real.Angle.tan θ = Real.Angle.tan ψ

theorem Real.Angle.tan_eq_of_two_zsmul_eq {θ : Real.Angle} {ψ : Real.Angle} (h : 2 • θ = 2 • ψ) : Real.Angle.tan θ = Real.Angle.tan ψ

theorem Real.Angle.tan_eq_inv_of_two_nsmul_add_two_nsmul_eq_pi {θ : Real.Angle} {ψ : Real.Angle} (h : 2 • θ + 2 • ψ = ↑Real.pi) : Real.Angle.tan ψ = (Real.Angle.tan θ)⁻¹

theorem Real.Angle.tan_eq_inv_of_two_zsmul_add_two_zsmul_eq_pi {θ : Real.Angle} {ψ : Real.Angle} (h : 2 • θ + 2 • ψ = ↑Real.pi) : Real.Angle.tan ψ = (Real.Angle.tan θ)⁻¹

def Real.Angle.sign (θ : Real.Angle) : SignType

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.

@[simp]

theorem Real.Angle.sign_zero : Real.Angle.sign 0 = 0

@[simp]

theorem Real.Angle.sign_coe_pi : Real.Angle.sign ↑Real.pi = 0

@[simp]

theorem Real.Angle.sign_neg (θ : Real.Angle) : Real.Angle.sign (-θ) = -Real.Angle.sign θ

theorem Real.Angle.sign_antiperiodic : Function.Antiperiodic Real.Angle.sign ↑Real.pi

@[simp]

theorem Real.Angle.sign_add_pi (θ : Real.Angle) : Real.Angle.sign (θ + ↑Real.pi) = -Real.Angle.sign θ

@[simp]

theorem Real.Angle.sign_pi_add (θ : Real.Angle) : Real.Angle.sign (↑Real.pi + θ) = -Real.Angle.sign θ

@[simp]

theorem Real.Angle.sign_sub_pi (θ : Real.Angle) : Real.Angle.sign (θ - ↑Real.pi) = -Real.Angle.sign θ

@[simp]

theorem Real.Angle.sign_pi_sub (θ : Real.Angle) : Real.Angle.sign (↑Real.pi - θ) = Real.Angle.sign θ

theorem Real.Angle.sign_eq_zero_iff {θ : Real.Angle} : Real.Angle.sign θ = 0 ↔ θ = 0 ∨ θ = ↑Real.pi

theorem Real.Angle.sign_ne_zero_iff {θ : Real.Angle} : Real.Angle.sign θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑Real.pi

theorem Real.Angle.toReal_neg_iff_sign_neg {θ : Real.Angle} : Real.Angle.toReal θ < 0 ↔ Real.Angle.sign θ = -1

theorem Real.Angle.toReal_nonneg_iff_sign_nonneg {θ : Real.Angle} : 0 ≤ Real.Angle.toReal θ ↔ 0 ≤ Real.Angle.sign θ

@[simp]

theorem Real.Angle.sign_toReal {θ : Real.Angle} (h : θ ≠ ↑Real.pi) : ↑SignType.sign (Real.Angle.toReal θ) = Real.Angle.sign θ

theorem Real.Angle.coe_abs_toReal_of_sign_nonneg {θ : Real.Angle} (h : 0 ≤ Real.Angle.sign θ) : ↑|Real.Angle.toReal θ| = θ

theorem Real.Angle.neg_coe_abs_toReal_of_sign_nonpos {θ : Real.Angle} (h : Real.Angle.sign θ ≤ 0) : -↑|Real.Angle.toReal θ| = θ

theorem Real.Angle.eq_iff_sign_eq_and_abs_toReal_eq {θ : Real.Angle} {ψ : Real.Angle} : θ = ψ ↔ Real.Angle.sign θ = Real.Angle.sign ψ ∧ |Real.Angle.toReal θ| = |Real.Angle.toReal ψ|

theorem Real.Angle.eq_iff_abs_toReal_eq_of_sign_eq {θ : Real.Angle} {ψ : Real.Angle} (h : Real.Angle.sign θ = Real.Angle.sign ψ) : θ = ψ ↔ |Real.Angle.toReal θ| = |Real.Angle.toReal ψ|

@[simp]

theorem Real.Angle.sign_coe_pi_div_two : Real.Angle.sign ↑(Real.pi / 2) = 1

@[simp]

theorem Real.Angle.sign_coe_neg_pi_div_two : Real.Angle.sign ↑(-Real.pi / 2) = -1

theorem Real.Angle.sign_coe_nonneg_of_nonneg_of_le_pi {θ : ℝ} (h0 : 0 ≤ θ) (hpi : θ ≤ Real.pi) : 0 ≤ Real.Angle.sign ↑θ

theorem Real.Angle.sign_neg_coe_nonpos_of_nonneg_of_le_pi {θ : ℝ} (h0 : 0 ≤ θ) (hpi : θ ≤ Real.pi) : Real.Angle.sign (-↑θ) ≤ 0

theorem Real.Angle.sign_two_nsmul_eq_sign_iff {θ : Real.Angle} : Real.Angle.sign (2 • θ) = Real.Angle.sign θ ↔ θ = ↑Real.pi ∨ |Real.Angle.toReal θ| < Real.pi / 2

theorem Real.Angle.sign_two_zsmul_eq_sign_iff {θ : Real.Angle} : Real.Angle.sign (2 • θ) = Real.Angle.sign θ ↔ θ = ↑Real.pi ∨ |Real.Angle.toReal θ| < Real.pi / 2

theorem Real.Angle.continuousAt_sign {θ : Real.Angle} (h0 : θ ≠ 0) (hpi : θ ≠ ↑Real.pi) : ContinuousAt Real.Angle.sign θ

theorem ContinuousOn.angle_sign_comp {α : Type u_1} [TopologicalSpace α] {f : α → Real.Angle} {s : Set α} (hf : ContinuousOn f s) (hs : ∀ (z : α), z ∈ s → f z ≠ 0 ∧ f z ≠ ↑Real.pi) : ContinuousOn (Real.Angle.sign ∘ f) s

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 ∈ s → f z ≠ 0 ∧ f z ≠ ↑Real.pi) (hx : x ∈ s) (hy : y ∈ s) : Real.Angle.sign (f y) = Real.Angle.sign (f x)

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.