mathlib3 documentation

analysis.special_functions.trigonometric.angle

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.

source
@[protected, instance]
noncomputable def real.angle.inhabited  :
inhabited real.angle
source
@[protected, instance]
noncomputable def real.angle.has_coe_t  :
has_coe_t ℝ real.angle
source
@[protected, instance]
noncomputable def real.angle.normed_add_comm_group  :
normed_add_comm_group real.angle
source
def real.angle  :
Type

The type of angles

Equations
Instances for real.angle
source
@[protected, instance]
noncomputable def real.angle.circular_order  :
circular_order real.angle
Equations
source
@[continuity]
theorem real.angle.continuous_coe  :
continuous coe
source
noncomputable def real.angle.coe_hom  :
ℝ →+ real.angle

Coercion ℝ → angle as an additive homomorphism.

Equations
source
@[simp]
theorem real.angle.coe_coe_hom  :
⇑real.angle.coe_hom = coe
source
@[protected]
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.

source
@[simp]
theorem real.angle.coe_zero  :
↑0 = 0
source
@[simp]
theorem real.angle.coe_add (x y : ℝ) :
↑(x + y) = ↑x + ↑y
source
@[simp]
theorem real.angle.coe_neg (x : ℝ) :
↑-x = -↑x
source
@[simp]
theorem real.angle.coe_sub (x y : ℝ) :
↑(x - y) = ↑x - ↑y
source
theorem real.angle.coe_nsmul (n : ℕ) (x : ℝ) :
↑(n • x) = n • ↑x
source
theorem real.angle.coe_zsmul (z : ℤ) (x : ℝ) :
↑(z • x) = z • ↑x
source
@[simp, norm_cast]
theorem real.angle.coe_nat_mul_eq_nsmul (x : ℝ) (n : ℕ) :
↑(↑n * x) = n • ↑x
source
@[simp, norm_cast]
theorem real.angle.coe_int_mul_eq_zsmul (x : ℝ) (n : ℤ) :
↑(↑n * x) = n • ↑x
source
theorem real.angle.angle_eq_iff_two_pi_dvd_sub {ψ θ : ℝ} :
↑θ = ↑ψ ↔ ∃ (k : ℤ), θ - ψ = 2 * real.pi * ↑k
source
@[simp]
theorem real.angle.coe_two_pi  :
↑(2 * real.pi) = 0
source
@[simp]
theorem real.angle.neg_coe_pi  :
-↑real.pi = ↑real.pi
source
@[simp]
theorem real.angle.two_nsmul_coe_div_two (θ : ℝ) :
2 • ↑(θ / 2) = ↑θ
source
@[simp]
theorem real.angle.two_zsmul_coe_div_two (θ : ℝ) :
2 • ↑(θ / 2) = ↑θ
source
@[simp]
theorem real.angle.two_nsmul_neg_pi_div_two  :
2 • ↑(-real.pi / 2) = ↑real.pi
source
@[simp]
theorem real.angle.two_zsmul_neg_pi_div_two  :
2 • ↑(-real.pi / 2) = ↑real.pi
source
theorem real.angle.sub_coe_pi_eq_add_coe_pi (θ : real.angle) :
θ - ↑real.pi = θ + ↑real.pi
source
@[simp]
theorem real.angle.two_nsmul_coe_pi  :
2 • ↑real.pi = 0
source
@[simp]
theorem real.angle.two_zsmul_coe_pi  :
2 • ↑real.pi = 0
source
@[simp]
theorem real.angle.coe_pi_add_coe_pi  :
↑real.pi + ↑real.pi = 0
source
theorem real.angle.zsmul_eq_iff {ψ θ : real.angle} {z : ℤ} (hz : z ≠ 0) :
z • ψ = z • θ ↔ ∃ (k : fin z.nat_abs), ψ = θ + ↑k • ↑(2 * real.pi / ↑z)
source
theorem real.angle.nsmul_eq_iff {ψ θ : real.angle} {n : ℕ} (hz : n ≠ 0) :
n • ψ = n • θ ↔ ∃ (k : fin n), ψ = θ + ↑k • ↑(2 * real.pi / ↑n)
source
theorem real.angle.two_zsmul_eq_iff {ψ θ : real.angle} :
2 • ψ = 2 • θ ↔ ψ = θ ∨ ψ = θ + ↑real.pi
source
theorem real.angle.two_nsmul_eq_iff {ψ θ : real.angle} :
2 • ψ = 2 • θ ↔ ψ = θ ∨ ψ = θ + ↑real.pi
source
theorem real.angle.two_nsmul_eq_zero_iff {θ : real.angle} :
2 • θ = 0 ↔ θ = 0 ∨ θ = ↑real.pi
source
theorem real.angle.two_nsmul_ne_zero_iff {θ : real.angle} :
2 • θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑real.pi
source
theorem real.angle.two_zsmul_eq_zero_iff {θ : real.angle} :
2 • θ = 0 ↔ θ = 0 ∨ θ = ↑real.pi
source
theorem real.angle.two_zsmul_ne_zero_iff {θ : real.angle} :
2 • θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑real.pi
source
theorem real.angle.eq_neg_self_iff {θ : real.angle} :
θ = -θ ↔ θ = 0 ∨ θ = ↑real.pi
source
theorem real.angle.ne_neg_self_iff {θ : real.angle} :
θ ≠ -θ ↔ θ ≠ 0 ∧ θ ≠ ↑real.pi
source
theorem real.angle.neg_eq_self_iff {θ : real.angle} :
-θ = θ ↔ θ = 0 ∨ θ = ↑real.pi
source
theorem real.angle.neg_ne_self_iff {θ : real.angle} :
-θ ≠ θ ↔ θ ≠ 0 ∧ θ ≠ ↑real.pi
source
theorem real.angle.two_nsmul_eq_pi_iff {θ : real.angle} :
2 • θ = ↑real.pi ↔ θ = ↑(real.pi / 2) ∨ θ = ↑(-real.pi / 2)
source
theorem real.angle.two_zsmul_eq_pi_iff {θ : real.angle} :
2 • θ = ↑real.pi ↔ θ = ↑(real.pi / 2) ∨ θ = ↑(-real.pi / 2)
source
theorem real.angle.cos_eq_iff_coe_eq_or_eq_neg {θ ψ : ℝ} :
real.cos θ = real.cos ψ ↔ ↑θ = ↑ψ ∨ ↑θ = -↑ψ
source
theorem real.angle.sin_eq_iff_coe_eq_or_add_eq_pi {θ ψ : ℝ} :
real.sin θ = real.sin ψ ↔ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑real.pi
source
theorem real.angle.cos_sin_inj {θ ψ : ℝ} (Hcos : real.cos θ = real.cos ψ) (Hsin : real.sin θ = real.sin ψ) :
↑θ = ↑ψ
source
noncomputable def real.angle.sin (θ : real.angle) :
ℝ

The sine of a real.angle.

Equations
source
@[simp]
theorem real.angle.sin_coe (x : ℝ) :
↑x.sin = real.sin x
source
@[continuity]
theorem real.angle.continuous_sin  :
continuous real.angle.sin
source
noncomputable def real.angle.cos (θ : real.angle) :
ℝ

The cosine of a real.angle.

Equations
source
@[simp]
theorem real.angle.cos_coe (x : ℝ) :
↑x.cos = real.cos x
source
@[continuity]
theorem real.angle.continuous_cos  :
continuous real.angle.cos
source
theorem real.angle.cos_eq_real_cos_iff_eq_or_eq_neg {θ : real.angle} {ψ : ℝ} :
θ.cos = real.cos ψ ↔ θ = ↑ψ ∨ θ = -↑ψ
source
theorem real.angle.cos_eq_iff_eq_or_eq_neg {θ ψ : real.angle} :
θ.cos = ψ.cos ↔ θ = ψ ∨ θ = -ψ
source
theorem real.angle.sin_eq_real_sin_iff_eq_or_add_eq_pi {θ : real.angle} {ψ : ℝ} :
θ.sin = real.sin ψ ↔ θ = ↑ψ ∨ θ + ↑ψ = ↑real.pi
source
theorem real.angle.sin_eq_iff_eq_or_add_eq_pi {θ ψ : real.angle} :
θ.sin = ψ.sin ↔ θ = ψ ∨ θ + ψ = ↑real.pi
source
@[simp]
theorem real.angle.sin_zero  :
0.sin = 0
source
@[simp]
theorem real.angle.sin_coe_pi  :
↑real.pi.sin = 0
source
theorem real.angle.sin_eq_zero_iff {θ : real.angle} :
θ.sin = 0 ↔ θ = 0 ∨ θ = ↑real.pi
source
theorem real.angle.sin_ne_zero_iff {θ : real.angle} :
θ.sin ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑real.pi
source
@[simp]
theorem real.angle.sin_neg (θ : real.angle) :
(-θ).sin = -θ.sin
source
theorem real.angle.sin_antiperiodic  :
function.antiperiodic real.angle.sin ↑real.pi
source
@[simp]
theorem real.angle.sin_add_pi (θ : real.angle) :
(θ + ↑real.pi).sin = -θ.sin
source
@[simp]
theorem real.angle.sin_sub_pi (θ : real.angle) :
(θ - ↑real.pi).sin = -θ.sin
source
@[simp]
theorem real.angle.cos_zero  :
0.cos = 1
source
@[simp]
theorem real.angle.cos_coe_pi  :
↑real.pi.cos = -1
source
@[simp]
theorem real.angle.cos_neg (θ : real.angle) :
(-θ).cos = θ.cos
source
theorem real.angle.cos_antiperiodic  :
function.antiperiodic real.angle.cos ↑real.pi
source
@[simp]
theorem real.angle.cos_add_pi (θ : real.angle) :
(θ + ↑real.pi).cos = -θ.cos
source
@[simp]
theorem real.angle.cos_sub_pi (θ : real.angle) :
(θ - ↑real.pi).cos = -θ.cos
source
theorem real.angle.cos_eq_zero_iff {θ : real.angle} :
θ.cos = 0 ↔ θ = ↑(real.pi / 2) ∨ θ = ↑(-real.pi / 2)
source
theorem real.angle.sin_add (θ₁ θ₂ : real.angle) :
(θ₁ + θ₂).sin = θ₁.sin * θ₂.cos + θ₁.cos * θ₂.sin
source
theorem real.angle.cos_add (θ₁ θ₂ : real.angle) :
(θ₁ + θ₂).cos = θ₁.cos * θ₂.cos - θ₁.sin * θ₂.sin
source
@[simp]
theorem real.angle.cos_sq_add_sin_sq (θ : real.angle) :
θ.cos ^ 2 + θ.sin ^ 2 = 1
source
theorem real.angle.sin_add_pi_div_two (θ : real.angle) :
(θ + ↑(real.pi / 2)).sin = θ.cos
source
theorem real.angle.sin_sub_pi_div_two (θ : real.angle) :
(θ - ↑(real.pi / 2)).sin = -θ.cos
source
theorem real.angle.sin_pi_div_two_sub (θ : real.angle) :
(↑(real.pi / 2) - θ).sin = θ.cos
source
theorem real.angle.cos_add_pi_div_two (θ : real.angle) :
(θ + ↑(real.pi / 2)).cos = -θ.sin
source
theorem real.angle.cos_sub_pi_div_two (θ : real.angle) :
(θ - ↑(real.pi / 2)).cos = θ.sin
source
theorem real.angle.cos_pi_div_two_sub (θ : real.angle) :
(↑(real.pi / 2) - θ).cos = θ.sin
source
theorem real.angle.abs_sin_eq_of_two_nsmul_eq {θ ψ : real.angle} (h : 2 • θ = 2 • ψ) :
|θ.sin| = |ψ.sin|
source
theorem real.angle.abs_sin_eq_of_two_zsmul_eq {θ ψ : real.angle} (h : 2 • θ = 2 • ψ) :
|θ.sin| = |ψ.sin|
source
theorem real.angle.abs_cos_eq_of_two_nsmul_eq {θ ψ : real.angle} (h : 2 • θ = 2 • ψ) :
|θ.cos| = |ψ.cos|
source
theorem real.angle.abs_cos_eq_of_two_zsmul_eq {θ ψ : real.angle} (h : 2 • θ = 2 • ψ) :
|θ.cos| = |ψ.cos|
source
@[simp]
theorem real.angle.coe_to_Ico_mod (θ ψ : ℝ) :
↑(to_Ico_mod real.two_pi_pos ψ θ) = ↑θ
source
@[simp]
theorem real.angle.coe_to_Ioc_mod (θ ψ : ℝ) :
↑(to_Ioc_mod real.two_pi_pos ψ θ) = ↑θ
source
noncomputable def real.angle.to_real (θ : real.angle) :
ℝ

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

Equations
source
theorem real.angle.to_real_coe (θ : ℝ) :
↑θ.to_real = to_Ioc_mod real.two_pi_pos (-real.pi) θ
source
theorem real.angle.to_real_coe_eq_self_iff {θ : ℝ} :
↑θ.to_real = θ ↔ -real.pi < θ ∧ θ ≤ real.pi
source
theorem real.angle.to_real_coe_eq_self_iff_mem_Ioc {θ : ℝ} :
↑θ.to_real = θ ↔ θ ∈ set.Ioc (-real.pi) real.pi
source
theorem real.angle.to_real_injective  :
function.injective real.angle.to_real
source
@[simp]
theorem real.angle.to_real_inj {θ ψ : real.angle} :
θ.to_real = ψ.to_real ↔ θ = ψ
source
@[simp]
theorem real.angle.coe_to_real (θ : real.angle) :
↑(θ.to_real) = θ
source
theorem real.angle.neg_pi_lt_to_real (θ : real.angle) :
-real.pi < θ.to_real
source
theorem real.angle.to_real_le_pi (θ : real.angle) :
θ.to_real ≤ real.pi
source
theorem real.angle.abs_to_real_le_pi (θ : real.angle) :
|θ.to_real| ≤ real.pi
source
theorem real.angle.to_real_mem_Ioc (θ : real.angle) :
θ.to_real ∈ set.Ioc (-real.pi) real.pi
source
@[simp]
theorem real.angle.to_Ioc_mod_to_real (θ : real.angle) :
to_Ioc_mod real.two_pi_pos (-real.pi) θ.to_real = θ.to_real
source
@[simp]
theorem real.angle.to_real_zero  :
0.to_real = 0
source
@[simp]
theorem real.angle.to_real_eq_zero_iff {θ : real.angle} :
θ.to_real = 0 ↔ θ = 0
source
@[simp]
theorem real.angle.to_real_pi  :
↑real.pi.to_real = real.pi
source
@[simp]
theorem real.angle.to_real_eq_pi_iff {θ : real.angle} :
θ.to_real = real.pi ↔ θ = ↑real.pi
source
theorem real.angle.pi_ne_zero  :
↑real.pi ≠ 0
source
@[simp]
theorem real.angle.to_real_pi_div_two  :
↑(real.pi / 2).to_real = real.pi / 2
source
@[simp]
theorem real.angle.to_real_eq_pi_div_two_iff {θ : real.angle} :
θ.to_real = real.pi / 2 ↔ θ = ↑(real.pi / 2)
source
@[simp]
theorem real.angle.to_real_neg_pi_div_two  :
↑(-real.pi / 2).to_real = -real.pi / 2
source
@[simp]
theorem real.angle.to_real_eq_neg_pi_div_two_iff {θ : real.angle} :
θ.to_real = -real.pi / 2 ↔ θ = ↑(-real.pi / 2)
source
theorem real.angle.pi_div_two_ne_zero  :
↑(real.pi / 2) ≠ 0
source
theorem real.angle.neg_pi_div_two_ne_zero  :
↑(-real.pi / 2) ≠ 0
source
theorem real.angle.abs_to_real_coe_eq_self_iff {θ : ℝ} :
|↑θ.to_real| = θ ↔ 0 ≤ θ ∧ θ ≤ real.pi
source
theorem real.angle.abs_to_real_neg_coe_eq_self_iff {θ : ℝ} :
|(-↑θ).to_real| = θ ↔ 0 ≤ θ ∧ θ ≤ real.pi
source
theorem real.angle.abs_to_real_eq_pi_div_two_iff {θ : real.angle} :
|θ.to_real| = real.pi / 2 ↔ θ = ↑(real.pi / 2) ∨ θ = ↑(-real.pi / 2)
source
theorem real.angle.nsmul_to_real_eq_mul {n : ℕ} (h : n ≠ 0) {θ : real.angle} :
(n • θ).to_real = ↑n * θ.to_real ↔ θ.to_real ∈ set.Ioc (-real.pi / ↑n) (real.pi / ↑n)
source
theorem real.angle.two_nsmul_to_real_eq_two_mul {θ : real.angle} :
(2 • θ).to_real = 2 * θ.to_real ↔ θ.to_real ∈ set.Ioc (-real.pi / 2) (real.pi / 2)
source
theorem real.angle.two_zsmul_to_real_eq_two_mul {θ : real.angle} :
(2 • θ).to_real = 2 * θ.to_real ↔ θ.to_real ∈ set.Ioc (-real.pi / 2) (real.pi / 2)
source
theorem real.angle.to_real_coe_eq_self_sub_two_mul_int_mul_pi_iff {θ : ℝ} {k : ℤ} :
↑θ.to_real = θ - 2 * ↑k * real.pi ↔ θ ∈ set.Ioc ((2 * ↑k - 1) * real.pi) ((2 * ↑k + 1) * real.pi)
source
theorem real.angle.to_real_coe_eq_self_sub_two_pi_iff {θ : ℝ} :
↑θ.to_real = θ - 2 * real.pi ↔ θ ∈ set.Ioc real.pi (3 * real.pi)
source
theorem real.angle.to_real_coe_eq_self_add_two_pi_iff {θ : ℝ} :
↑θ.to_real = θ + 2 * real.pi ↔ θ ∈ set.Ioc ((-3) * real.pi) (-real.pi)
source
theorem real.angle.two_nsmul_to_real_eq_two_mul_sub_two_pi {θ : real.angle} :
(2 • θ).to_real = 2 * θ.to_real - 2 * real.pi ↔ real.pi / 2 < θ.to_real
source
theorem real.angle.two_zsmul_to_real_eq_two_mul_sub_two_pi {θ : real.angle} :
(2 • θ).to_real = 2 * θ.to_real - 2 * real.pi ↔ real.pi / 2 < θ.to_real
source
theorem real.angle.two_nsmul_to_real_eq_two_mul_add_two_pi {θ : real.angle} :
(2 • θ).to_real = 2 * θ.to_real + 2 * real.pi ↔ θ.to_real ≤ -real.pi / 2
source
theorem real.angle.two_zsmul_to_real_eq_two_mul_add_two_pi {θ : real.angle} :
(2 • θ).to_real = 2 * θ.to_real + 2 * real.pi ↔ θ.to_real ≤ -real.pi / 2
source
@[simp]
theorem real.angle.sin_to_real (θ : real.angle) :
real.sin θ.to_real = θ.sin
source
@[simp]
theorem real.angle.cos_to_real (θ : real.angle) :
real.cos θ.to_real = θ.cos
source
theorem real.angle.cos_nonneg_iff_abs_to_real_le_pi_div_two {θ : real.angle} :
0 ≤ θ.cos ↔ |θ.to_real| ≤ real.pi / 2
source
theorem real.angle.cos_pos_iff_abs_to_real_lt_pi_div_two {θ : real.angle} :
0 < θ.cos ↔ |θ.to_real| < real.pi / 2
source
theorem real.angle.cos_neg_iff_pi_div_two_lt_abs_to_real {θ : real.angle} :
θ.cos < 0 ↔ real.pi / 2 < |θ.to_real|
source
theorem real.angle.abs_cos_eq_abs_sin_of_two_nsmul_add_two_nsmul_eq_pi {θ ψ : real.angle} (h : 2 • θ + 2 • ψ = ↑real.pi) :
|θ.cos| = |ψ.sin|
source
theorem real.angle.abs_cos_eq_abs_sin_of_two_zsmul_add_two_zsmul_eq_pi {θ ψ : real.angle} (h : 2 • θ + 2 • ψ = ↑real.pi) :
|θ.cos| = |ψ.sin|
source
noncomputable def real.angle.tan (θ : real.angle) :
ℝ

The tangent of a real.angle.

Equations
source
theorem real.angle.tan_eq_sin_div_cos (θ : real.angle) :
θ.tan = θ.sin / θ.cos
source
@[simp]
theorem real.angle.tan_coe (x : ℝ) :
↑x.tan = real.tan x
source
@[simp]
theorem real.angle.tan_zero  :
0.tan = 0
source
@[simp]
theorem real.angle.tan_coe_pi  :
↑real.pi.tan = 0
source
theorem real.angle.tan_periodic  :
function.periodic real.angle.tan ↑real.pi
source
@[simp]
theorem real.angle.tan_add_pi (θ : real.angle) :
(θ + ↑real.pi).tan = θ.tan
source
@[simp]
theorem real.angle.tan_sub_pi (θ : real.angle) :
(θ - ↑real.pi).tan = θ.tan
source
@[simp]
theorem real.angle.tan_to_real (θ : real.angle) :
real.tan θ.to_real = θ.tan
source
theorem real.angle.tan_eq_of_two_nsmul_eq {θ ψ : real.angle} (h : 2 • θ = 2 • ψ) :
θ.tan = ψ.tan
source
theorem real.angle.tan_eq_of_two_zsmul_eq {θ ψ : real.angle} (h : 2 • θ = 2 • ψ) :
θ.tan = ψ.tan
source
theorem real.angle.tan_eq_inv_of_two_nsmul_add_two_nsmul_eq_pi {θ ψ : real.angle} (h : 2 • θ + 2 • ψ = ↑real.pi) :
ψ.tan = (θ.tan)⁻¹
source
theorem real.angle.tan_eq_inv_of_two_zsmul_add_two_zsmul_eq_pi {θ ψ : real.angle} (h : 2 • θ + 2 • ψ = ↑real.pi) :
ψ.tan = (θ.tan)⁻¹
source
noncomputable def real.angle.sign (θ : real.angle) :
sign_type

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
source
@[simp]
theorem real.angle.sign_zero  :
0.sign = 0
source
@[simp]
theorem real.angle.sign_coe_pi  :
↑real.pi.sign = 0
source
@[simp]
theorem real.angle.sign_neg (θ : real.angle) :
(-θ).sign = -θ.sign
source
theorem real.angle.sign_antiperiodic  :
function.antiperiodic real.angle.sign ↑real.pi
source
@[simp]
theorem real.angle.sign_add_pi (θ : real.angle) :
(θ + ↑real.pi).sign = -θ.sign
source
@[simp]
theorem real.angle.sign_pi_add (θ : real.angle) :
(↑real.pi + θ).sign = -θ.sign
source
@[simp]
theorem real.angle.sign_sub_pi (θ : real.angle) :
(θ - ↑real.pi).sign = -θ.sign
source
@[simp]
theorem real.angle.sign_pi_sub (θ : real.angle) :
(↑real.pi - θ).sign = θ.sign
source
theorem real.angle.sign_eq_zero_iff {θ : real.angle} :
θ.sign = 0 ↔ θ = 0 ∨ θ = ↑real.pi
source
theorem real.angle.sign_ne_zero_iff {θ : real.angle} :
θ.sign ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑real.pi
source
theorem real.angle.to_real_neg_iff_sign_neg {θ : real.angle} :
θ.to_real < 0 ↔ θ.sign = -1
source
theorem real.angle.to_real_nonneg_iff_sign_nonneg {θ : real.angle} :
0 ≤ θ.to_real ↔ 0 ≤ θ.sign
source
@[simp]
theorem real.angle.sign_to_real {θ : real.angle} (h : θ ≠ ↑real.pi) :
⇑sign θ.to_real = θ.sign
source
theorem real.angle.coe_abs_to_real_of_sign_nonneg {θ : real.angle} (h : 0 ≤ θ.sign) :
↑|θ.to_real| = θ
source
theorem real.angle.neg_coe_abs_to_real_of_sign_nonpos {θ : real.angle} (h : θ.sign ≤ 0) :
-↑|θ.to_real| = θ
source
theorem real.angle.eq_iff_sign_eq_and_abs_to_real_eq {θ ψ : real.angle} :
θ = ψ ↔ θ.sign = ψ.sign ∧ |θ.to_real| = |ψ.to_real|
source
theorem real.angle.eq_iff_abs_to_real_eq_of_sign_eq {θ ψ : real.angle} (h : θ.sign = ψ.sign) :
θ = ψ ↔ |θ.to_real| = |ψ.to_real|
source
@[simp]
theorem real.angle.sign_coe_pi_div_two  :
↑(real.pi / 2).sign = 1
source
@[simp]
theorem real.angle.sign_coe_neg_pi_div_two  :
↑(-real.pi / 2).sign = -1
source
theorem real.angle.sign_coe_nonneg_of_nonneg_of_le_pi {θ : ℝ} (h0 : 0 ≤ θ) (hpi : θ ≤ real.pi) :
0 ≤ ↑θ.sign
source
theorem real.angle.sign_neg_coe_nonpos_of_nonneg_of_le_pi {θ : ℝ} (h0 : 0 ≤ θ) (hpi : θ ≤ real.pi) :
(-↑θ).sign ≤ 0
source
theorem real.angle.sign_two_nsmul_eq_sign_iff {θ : real.angle} :
(2 • θ).sign = θ.sign ↔ θ = ↑real.pi ∨ |θ.to_real| < real.pi / 2
source
theorem real.angle.sign_two_zsmul_eq_sign_iff {θ : real.angle} :
(2 • θ).sign = θ.sign ↔ θ = ↑real.pi ∨ |θ.to_real| < real.pi / 2
source
theorem real.angle.continuous_at_sign {θ : real.angle} (h0 : θ ≠ 0) (hpi : θ ≠ ↑real.pi) :
continuous_at real.angle.sign θ
source
theorem continuous_on.angle_sign_comp {α : Type u_1} [topological_space α] {f : α → real.angle} {s : set α} (hf : continuous_on f s) (hs : ∀ (z : α), z ∈ s → f z ≠ 0 ∧ f z ≠ ↑real.pi) :
continuous_on (real.angle.sign ∘ f) s
source
theorem real.angle.sign_eq_of_continuous_on {α : Type u_1} [topological_space α] {f : α → real.angle} {s : set α} {x y : α} (hc : is_connected s) (hf : continuous_on f s) (hs : ∀ (z : α), 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.