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

@[implicit_reducible]

noncomputable instance Real.instNormedAddCommGroupAngle : NormedAddCommGroup Angle

@[implicit_reducible]

noncomputable instance Real.instInhabitedAngle : Inhabited Angle

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

The canonical map from ℝ to the quotient Angle.

@[implicit_reducible]

noncomputable instance Real.Angle.instCoe : Coe ℝ Angle

@[implicit_reducible]

instance Real.Angle.instCircularOrder : CircularOrder Angle

theorem Real.Angle.continuous_coe : Continuous Angle.coe

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

Coercion ℝ → Angle as an additive homomorphism.

@[simp]

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

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

theorem Real.Angle.coe_eq_zero_iff {x : ℝ} : ↑x = 0 ↔ ∃ (n : ℤ), n • (2 * Real.pi) = x

@[simp]

theorem Real.Angle.natCast_mul_eq_nsmul (x : ℝ) (n : ℕ) : ↑(↑n * x) = n • ↑x

@[simp]

theorem Real.Angle.intCast_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 (θ : 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 {ψ θ : Angle} {z : ℤ} (hz : z ≠ 0) : z • ψ = z • θ ↔ ∃ (k : Fin z.natAbs), ψ = θ + ↑k • ↑(2 * Real.pi / ↑z)

theorem Real.Angle.nsmul_eq_iff {ψ θ : Angle} {n : ℕ} (hz : n ≠ 0) : n • ψ = n • θ ↔ ∃ (k : Fin n), ψ = θ + ↑k • ↑(2 * Real.pi / ↑n)

theorem Real.Angle.two_zsmul_eq_iff {ψ θ : Angle} : 2 • ψ = 2 • θ ↔ ψ = θ ∨ ψ = θ + ↑Real.pi

theorem Real.Angle.two_nsmul_eq_iff {ψ θ : Angle} : 2 • ψ = 2 • θ ↔ ψ = θ ∨ ψ = θ + ↑Real.pi

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

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

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

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

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

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

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

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

theorem Real.Angle.two_nsmul_eq_pi_iff {θ : Angle} : 2 • θ = ↑Real.pi ↔ θ = ↑(Real.pi / 2) ∨ θ = ↑(-Real.pi / 2)

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

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

The sine of a Real.Angle.

@[simp]

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

theorem Real.Angle.continuous_sin : Continuous sin

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

The cosine of a Real.Angle.

@[simp]

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

theorem Real.Angle.continuous_cos : Continuous cos

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

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

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

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

@[simp]

theorem Real.Angle.sin_zero : sin 0 = 0

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

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem Real.Angle.cos_zero : cos 0 = 1

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

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

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

theorem Real.Angle.sin_two_nsmul (θ : Angle) : (2 • θ).sin = 2 • (θ.sin * θ.cos)

@[simp]

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

theorem Real.Angle.toReal_injective : Function.Injective toReal

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

theorem Real.Angle.toReal_zero : toReal 0 = 0

@[simp]

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

@[simp]

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

@[simp]

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

theorem Real.Angle.toReal_neg_eq_neg_toReal_iff {θ : Angle} : (-θ).toReal = -θ.toReal ↔ θ ≠ ↑Real.pi

@[simp]

theorem Real.Angle.abs_toReal_neg (θ : Angle) : |(-θ).toReal| = |θ.toReal|

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Real.Angle.toReal_eq_neg_pi_div_two_iff {θ : 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 {θ : ℝ} : |(↑θ).toReal| = θ ↔ 0 ≤ θ ∧ θ ≤ Real.pi

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

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

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

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

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

theorem Real.Angle.toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff {θ : ℝ} {k : ℤ} : (↑θ).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 {θ : ℝ} : (↑θ).toReal = θ - 2 * Real.pi ↔ θ ∈ Set.Ioc Real.pi (3 * Real.pi)

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

theorem Real.Angle.two_nsmul_eq_iff_eq_of_abs_toReal_lt_pi_div_two {θ ψ : Angle} (hθ : |θ.toReal| < Real.pi / 2) (hψ : |ψ.toReal| < Real.pi / 2) : 2 • θ = 2 • ψ ↔ θ = ψ

theorem Real.Angle.two_zsmul_eq_iff_eq_of_abs_toReal_lt_pi_div_two {θ ψ : Angle} (hθ : |θ.toReal| < Real.pi / 2) (hψ : |ψ.toReal| < Real.pi / 2) : 2 • θ = 2 • ψ ↔ θ = ψ

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

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

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

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

The tangent of a Real.Angle.

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

@[simp]

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

@[simp]

theorem Real.Angle.tan_zero : tan 0 = 0

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

noncomputable def Real.Angle.sign (θ : 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 : sign 0 = 0

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

theorem Real.Angle.toReal_mem_Ioo_iff_sign_pos {θ : Angle} : θ.toReal ∈ Set.Ioo 0 Real.pi ↔ θ.sign = 1

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

theorem Real.Angle.eq_add_pi_of_two_zsmul_eq_of_sign_eq_neg (a b : Angle) (h : 2 • a = 2 • b) (h_sign : a.sign = -b.sign) (h_ne : b.sign ≠ 0) : a = b + ↑Real.pi

theorem Real.Angle.sub_ne_pi_of_sign_eq_of_sign_ne_zero (a b : Angle) (h_sign : a.sign = b.sign) (h_ne : b.sign ≠ 0) : a - b ≠ ↑Real.pi

theorem Real.Angle.two_zsmul_eq_iff_eq {a b : Angle} (ha : a.sign ≠ 0) (h : a.sign = b.sign) : 2 • a = 2 • b ↔ a = b

theorem Real.Angle.abs_toReal_add_abs_toReal_eq_pi_of_two_nsmul_add_eq_zero_of_sign_eq {θ ψ : Angle} (h : 2 • (θ + ψ) = 0) (hs : θ.sign = ψ.sign) (h0 : θ.sign ≠ 0) : |θ.toReal| + |ψ.toReal| = Real.pi

theorem Real.Angle.abs_toReal_add_abs_toReal_eq_pi_of_two_zsmul_add_eq_zero_of_sign_eq {θ ψ : Angle} (h : 2 • (θ + ψ) = 0) (hs : θ.sign = ψ.sign) (h0 : θ.sign ≠ 0) : |θ.toReal| + |ψ.toReal| = Real.pi

theorem Real.Angle.toReal_add_of_sign_pos_sign_neg {θ ψ : Angle} (hθ : θ.sign = 1) (hψ : ψ.sign = -1) : (θ + ψ).toReal = θ.toReal + ψ.toReal

theorem Real.Angle.toReal_add_of_sign_eq_neg_sign {θ ψ : Angle} (hψ : θ ≠ ↑Real.pi ∨ ψ ≠ ↑Real.pi) (hs : θ.sign = -ψ.sign) : (θ + ψ).toReal = θ.toReal + ψ.toReal

theorem Real.Angle.toReal_add_eq_toReal_add_toReal {θ ψ : Angle} (hθ : θ ≠ ↑Real.pi) (hψ : ψ ≠ ↑Real.pi) (hs : θ.sign ≠ ψ.sign ∨ θ.sign = (θ + ψ).sign) : (θ + ψ).toReal = θ.toReal + ψ.toReal

theorem Real.Angle.abs_toReal_add_eq_two_pi_sub_abs_toReal_add_abs_toReal {θ ψ : Angle} (hs : θ.sign = ψ.sign) (hsa : θ.sign ≠ (θ + ψ).sign) : |(θ + ψ).toReal| = 2 * Real.pi - (|θ.toReal| + |ψ.toReal|)

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

theorem ContinuousOn.angle_sign_comp {α : Type u_1} [TopologicalSpace α] {f : α → Real.Angle} {s : Set α} (hf : ContinuousOn f s) (hs : ∀ 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 : α → Angle} {s : Set α} {x y : α} (hc : IsConnected s) (hf : ContinuousOn f s) (hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ ↑Real.pi) (hx : x ∈ s) (hy : y ∈ s) : (f y).sign = (f x).sign

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.