# mathlib3documentation

analysis.special_functions.trigonometric.inverse

# Inverse trigonometric functions. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

See also analysis.special_functions.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
theorem real.arcsin_mem_Icc (x : ) :
@[simp]
theorem real.range_arcsin  :
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.inj_on_arcsin  :
(set.Icc (-1) 1)
theorem real.arcsin_inj {x y : } (hx₁ : -1 x) (hx₂ : x 1) (hy₁ : -1 y) (hy₂ : y 1) :
x = y
@[continuity]
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]
theorem real.neg_pi_div_two_lt_arcsin {x : } :
-(real.pi / 2) < -1 < x
@[simp]
theorem real.arcsin_eq_pi_div_two {x : } :
= 1 x
@[simp]
theorem real.pi_div_two_eq_arcsin {x : } :
= 1 x
@[simp]
theorem real.pi_div_two_le_arcsin {x : } :
1 x
@[simp]
theorem real.arcsin_eq_neg_pi_div_two {x : } :
= -(real.pi / 2) x -1
@[simp]
theorem real.neg_pi_div_two_eq_arcsin {x : } :
-(real.pi / 2) = x -1
@[simp]
theorem real.arcsin_le_neg_pi_div_two {x : } :
-(real.pi / 2) x -1
@[simp]
theorem real.pi_div_four_le_arcsin {x : } :
2 / 2 x
theorem real.maps_to_sin_Ioo  :
(set.Ioo (-(real.pi / 2)) (real.pi / 2)) (set.Ioo (-1) 1)
@[simp]
noncomputable def real.sin_local_homeomorph  :

real.sin as a local_homeomorph between (-π / 2, π / 2) and (-1, 1).

Equations
theorem real.cos_arcsin_nonneg (x : ) :
0
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
theorem real.arccos_le_pi (x : ) :
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 real.pi) :
= x
theorem real.arccos_inj_on  :
(set.Icc (-1) 1)
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]
@[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_neg (x : ) :
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]
theorem real.arccos_le_pi_div_two {x : } :
0 x
@[simp]
theorem real.arccos_lt_pi_div_two {x : } :
< 0 < x
@[simp]
theorem real.arccos_le_pi_div_four {x : } :
2 / 2 x
@[continuity]
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))