mathlib3 documentation

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.sin_arcsin' {x : } (hx : x set.Icc (-1) 1) :
theorem real.sin_arcsin {x : } (hx₁ : -1 x) (hx₂ : x 1) :
theorem real.arcsin_sin' {x : } (hx : x set.Icc (-(real.pi / 2)) (real.pi / 2)) :
theorem real.arcsin_sin {x : } (hx₁ : -(real.pi / 2) x) (hx₂ : x real.pi / 2) :
theorem real.arcsin_inj {x y : } (hx₁ : -1 x) (hx₂ : x 1) (hy₁ : -1 y) (hy₂ : y 1) :
theorem real.arcsin_eq_of_sin_eq {x y : } (h₁ : real.sin x = y) (h₂ : x set.Icc (-(real.pi / 2)) (real.pi / 2)) :
@[simp]
theorem real.arcsin_zero  :
@[simp]
theorem real.arcsin_of_one_le {x : } (hx : 1 x) :
theorem real.arcsin_of_le_neg_one {x : } (hx : x -1) :
@[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)) :
theorem real.arcsin_le_iff_le_sin' {x y : } (hy : y set.Ico (-(real.pi / 2)) (real.pi / 2)) :
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) :
theorem real.le_arcsin_iff_sin_le' {x y : } (hx : x set.Ioc (-(real.pi / 2)) (real.pi / 2)) :
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)) :
theorem real.arcsin_lt_iff_lt_sin' {x y : } (hy : y set.Ioc (-(real.pi / 2)) (real.pi / 2)) :
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) :
theorem real.lt_arcsin_iff_sin_lt' {x y : } (hx : x set.Ico (-(real.pi / 2)) (real.pi / 2)) :
theorem real.arcsin_eq_iff_eq_sin {x y : } (hy : y set.Ioo (-(real.pi / 2)) (real.pi / 2)) :
@[simp]
theorem real.arcsin_nonneg {x : } :
@[simp]
theorem real.arcsin_nonpos {x : } :
@[simp]
theorem real.arcsin_eq_zero_iff {x : } :
real.arcsin x = 0 x = 0
@[simp]
theorem real.zero_eq_arcsin_iff {x : } :
0 = real.arcsin x x = 0
@[simp]
theorem real.arcsin_pos {x : } :
0 < real.arcsin x 0 < x
@[simp]
theorem real.arcsin_lt_zero {x : } :
real.arcsin x < 0 x < 0
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]

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

Equations
theorem real.cos_arcsin (x : ) :
real.cos (real.arcsin x) = (1 - x ^ 2)
theorem real.tan_arcsin (x : ) :
real.tan (real.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
@[simp]
theorem real.arccos_pos {x : } :
0 < real.arccos x x < 1
theorem real.cos_arccos {x : } (hx₁ : -1 x) (hx₂ : x 1) :
theorem real.arccos_cos {x : } (hx₁ : 0 x) (hx₂ : x real.pi) :
theorem real.arccos_inj {x y : } (hx₁ : -1 x) (hx₂ : x 1) (hy₁ : -1 y) (hy₂ : y 1) :
@[simp]
@[simp]
theorem real.arccos_one  :
@[simp]
@[simp]
theorem real.arccos_eq_zero {x : } :
@[simp]
@[simp]
theorem real.arccos_eq_pi {x : } :
theorem real.arccos_of_one_le {x : } (hx : 1 x) :
theorem real.arccos_of_le_neg_one {x : } (hx : x -1) :
theorem real.sin_arccos (x : ) :
real.sin (real.arccos x) = (1 - x ^ 2)
@[simp]
@[simp]
@[simp]
theorem real.tan_arccos (x : ) :
real.tan (real.arccos x) = (1 - x ^ 2) / x
theorem real.arccos_eq_arcsin {x : } (h : 0 x) :
theorem real.arcsin_eq_arccos {x : } (h : 0 x) :