# Inverse trigonometric functions. #

See also Analysis.SpecialFunctions.Trigonometric.Arctan for the inverse tan function. (This is delayed as it is easier to set up after developing complex trigonometric functions.)

Basic inequalities on trigonometric functions.

noncomputable def Real.arcsin :

Inverse of the sin function, returns values in the range -π / 2 ≤ arcsin x ≤ π / 2. It defaults to -π / 2 on (-∞, -1) and to π / 2 to (1, ∞).

Equations
Instances For
@[simp]
theorem Real.arcsin_projIcc (x : ) :
Real.arcsin (Set.projIcc (-1) 1 x) =
theorem Real.sin_arcsin' {x : } (hx : x Set.Icc (-1) 1) :
= x
theorem Real.sin_arcsin {x : } (hx₁ : -1 x) (hx₂ : x 1) :
= x
theorem Real.arcsin_sin' {x : } (hx : x Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) :
= x
theorem Real.arcsin_sin {x : } (hx₁ : -(Real.pi / 2) x) (hx₂ : x ) :
= x
theorem Real.arcsin_inj {x : } {y : } (hx₁ : -1 x) (hx₂ : x 1) (hy₁ : -1 y) (hy₂ : y 1) :
x = y
theorem Real.arcsin_eq_of_sin_eq {x : } {y : } (h₁ : = y) (h₂ : x Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) :
= x
@[simp]
theorem Real.arcsin_zero :
= 0
@[simp]
theorem Real.arcsin_one :
=
theorem Real.arcsin_of_one_le {x : } (hx : 1 x) :
=
theorem Real.arcsin_of_le_neg_one {x : } (hx : x -1) :
= -(Real.pi / 2)
@[simp]
theorem Real.arcsin_neg (x : ) :
theorem Real.arcsin_le_iff_le_sin {x : } {y : } (hx : x Set.Icc (-1) 1) (hy : y Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) :
y x
theorem Real.arcsin_le_iff_le_sin' {x : } {y : } (hy : y Set.Ico (-(Real.pi / 2)) (Real.pi / 2)) :
y x
theorem Real.le_arcsin_iff_sin_le {x : } {y : } (hx : x Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) (hy : y Set.Icc (-1) 1) :
x y
theorem Real.le_arcsin_iff_sin_le' {x : } {y : } (hx : x Set.Ioc (-(Real.pi / 2)) (Real.pi / 2)) :
x y
theorem Real.arcsin_lt_iff_lt_sin {x : } {y : } (hx : x Set.Icc (-1) 1) (hy : y Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) :
< y x <
theorem Real.arcsin_lt_iff_lt_sin' {x : } {y : } (hy : y Set.Ioc (-(Real.pi / 2)) (Real.pi / 2)) :
< y x <
theorem Real.lt_arcsin_iff_sin_lt {x : } {y : } (hx : x Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) (hy : y Set.Icc (-1) 1) :
x < < y
theorem Real.lt_arcsin_iff_sin_lt' {x : } {y : } (hx : x Set.Ico (-(Real.pi / 2)) (Real.pi / 2)) :
x < < y
theorem Real.arcsin_eq_iff_eq_sin {x : } {y : } (hy : y Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)) :
= y x =
@[simp]
theorem Real.arcsin_nonneg {x : } :
0 0 x
@[simp]
theorem Real.arcsin_nonpos {x : } :
0 x 0
@[simp]
theorem Real.arcsin_eq_zero_iff {x : } :
= 0 x = 0
@[simp]
theorem Real.zero_eq_arcsin_iff {x : } :
0 = x = 0
@[simp]
theorem Real.arcsin_pos {x : } :
0 < 0 < x
@[simp]
theorem Real.arcsin_lt_zero {x : } :
< 0 x < 0
@[simp]
theorem Real.arcsin_lt_pi_div_two {x : } :
< x < 1
@[simp]
@[simp]
theorem Real.arcsin_eq_pi_div_two {x : } :
= 1 x
@[simp]
theorem Real.pi_div_two_eq_arcsin {x : } :
= 1 x
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]

Real.sin as a PartialHomeomorph between (-π / 2, π / 2) and (-1, 1).

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Real.cos_arcsin (x : ) :
= (1 - x ^ 2)
theorem Real.tan_arcsin (x : ) :
= x / (1 - x ^ 2)
noncomputable def Real.arccos (x : ) :

Inverse of the cos function, returns values in the range 0 ≤ arccos x and arccos x ≤ π. It defaults to π on (-∞, -1) and to 0 to (1, ∞).

Equations
Instances For
theorem Real.arccos_nonneg (x : ) :
0
@[simp]
theorem Real.arccos_pos {x : } :
0 < x < 1
theorem Real.cos_arccos {x : } (hx₁ : -1 x) (hx₂ : x 1) :
= x
theorem Real.arccos_cos {x : } (hx₁ : 0 x) (hx₂ : ) :
= x
theorem Real.arccos_eq_of_eq_cos {x : } {y : } (hy₀ : 0 y) (hy₁ : ) (hxy : x = ) :
= y
theorem Real.arccos_inj {x : } {y : } (hx₁ : -1 x) (hx₂ : x 1) (hy₁ : -1 y) (hy₂ : y 1) :
x = y
@[simp]
theorem Real.arccos_zero :
=
@[simp]
theorem Real.arccos_one :
= 0
@[simp]
theorem Real.arccos_eq_zero {x : } :
= 0 1 x
@[simp]
theorem Real.arccos_eq_pi_div_two {x : } :
= x = 0
@[simp]
theorem Real.arccos_eq_pi {x : } :
x -1
theorem Real.arccos_of_one_le {x : } (hx : 1 x) :
= 0
theorem Real.arccos_of_le_neg_one {x : } (hx : x -1) :
theorem Real.sin_arccos (x : ) :
= (1 - x ^ 2)
@[simp]
@[simp]
theorem Real.arccos_lt_pi_div_two {x : } :
< 0 < x
@[simp]
theorem Real.tan_arccos (x : ) :
= (1 - x ^ 2) / x
theorem Real.arccos_eq_arcsin {x : } (h : 0 x) :
= Real.arcsin (1 - x ^ 2)
theorem Real.arcsin_eq_arccos {x : } (h : 0 x) :
= Real.arccos (1 - x ^ 2)