# 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.

source
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

- Real.arcsin = Subtype.val ∘ Set.IccExtend Real.arcsin._proof_2 ⇑Real.sinOrderIso.symm

Instances For

source
theorem Real.arcsin_mem_Icc (x : ℝ) :
arcsin x ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2)
source
@[simp]
theorem Real.range_arcsin :
Set.range arcsin = Set.Icc (-(Real.pi / 2)) (Real.pi / 2)
source
theorem Real.arcsin_le_pi_div_two (x : ℝ) :
arcsin x ≤ Real.pi / 2
source
theorem Real.neg_pi_div_two_le_arcsin (x : ℝ) :
-(Real.pi / 2) ≤ arcsin x
source
theorem Real.arcsin_projIcc (x : ℝ) :
arcsin ↑(Set.projIcc (-1) 1 ⋯ x) = arcsin x
source
theorem Real.sin_arcsin' {x : ℝ} (hx : x ∈ Set.Icc (-1) 1) :
sin (arcsin x) = x
source
theorem Real.sin_arcsin {x : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) :
sin (arcsin x) = x
source
theorem Real.arcsin_sin' {x : ℝ} (hx : x ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) :
arcsin (sin x) = x
source
theorem Real.arcsin_sin {x : ℝ} (hx₁ : -(Real.pi / 2) ≤ x) (hx₂ : x ≤ Real.pi / 2) :
arcsin (sin x) = x
source
theorem Real.strictMonoOn_arcsin :
StrictMonoOn arcsin (Set.Icc (-1) 1)
source
theorem Real.arcsin_lt_arcsin {x y : ℝ} (hx : -1 ≤ x) (hlt : x < y) (hy : y ≤ 1) :
arcsin x < arcsin y
source
theorem Real.monotone_arcsin :
Monotone arcsin
source
theorem Real.arcsin_le_arcsin {x y : ℝ} (h : x ≤ y) :
arcsin x ≤ arcsin y
source
theorem Real.injOn_arcsin :
Set.InjOn arcsin (Set.Icc (-1) 1)
source
theorem Real.arcsin_inj {x y : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) (hy₁ : -1 ≤ y) (hy₂ : y ≤ 1) :
arcsin x = arcsin y ↔ x = y
source
theorem Real.continuous_arcsin :
Continuous arcsin
source
theorem Real.continuousAt_arcsin {x : ℝ} :
ContinuousAt arcsin x
source
theorem Real.arcsin_eq_of_sin_eq {x y : ℝ} (h₁ : sin x = y) (h₂ : x ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) :
arcsin y = x
source
@[simp]
theorem Real.arcsin_zero :
arcsin 0 = 0
source
@[simp]
theorem Real.arcsin_one :
arcsin 1 = Real.pi / 2
source
theorem Real.arcsin_of_one_le {x : ℝ} (hx : 1 ≤ x) :
arcsin x = Real.pi / 2
source
theorem Real.arcsin_neg_one :
arcsin (-1) = -(Real.pi / 2)
source
theorem Real.arcsin_of_le_neg_one {x : ℝ} (hx : x ≤ -1) :
arcsin x = -(Real.pi / 2)
source
@[simp]
theorem Real.arcsin_neg (x : ℝ) :
arcsin (-x) = -arcsin x
source
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)) :
arcsin x ≤ y ↔ x ≤ sin y
source
theorem Real.arcsin_le_iff_le_sin' {x y : ℝ} (hy : y ∈ Set.Ico (-(Real.pi / 2)) (Real.pi / 2)) :
arcsin x ≤ y ↔ x ≤ sin y
source
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 ≤ arcsin y ↔ sin x ≤ y
source
theorem Real.le_arcsin_iff_sin_le' {x y : ℝ} (hx : x ∈ Set.Ioc (-(Real.pi / 2)) (Real.pi / 2)) :
x ≤ arcsin y ↔ sin x ≤ y
source
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)) :
arcsin x < y ↔ x < sin y
source
theorem Real.arcsin_lt_iff_lt_sin' {x y : ℝ} (hy : y ∈ Set.Ioc (-(Real.pi / 2)) (Real.pi / 2)) :
arcsin x < y ↔ x < sin y
source
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 < arcsin y ↔ sin x < y
source
theorem Real.lt_arcsin_iff_sin_lt' {x y : ℝ} (hx : x ∈ Set.Ico (-(Real.pi / 2)) (Real.pi / 2)) :
x < arcsin y ↔ sin x < y
source
theorem Real.arcsin_eq_iff_eq_sin {x y : ℝ} (hy : y ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)) :
arcsin x = y ↔ x = sin y
source
@[simp]
theorem Real.arcsin_nonneg {x : ℝ} :
0 ≤ arcsin x ↔ 0 ≤ x
source
@[simp]
theorem Real.arcsin_nonpos {x : ℝ} :
arcsin x ≤ 0 ↔ x ≤ 0
source
@[simp]
theorem Real.arcsin_eq_zero_iff {x : ℝ} :
arcsin x = 0 ↔ x = 0
source
@[simp]
theorem Real.zero_eq_arcsin_iff {x : ℝ} :
0 = arcsin x ↔ x = 0
source
@[simp]
theorem Real.arcsin_pos {x : ℝ} :
0 < arcsin x ↔ 0 < x
source
@[simp]
theorem Real.arcsin_lt_zero {x : ℝ} :
arcsin x < 0 ↔ x < 0
source
@[simp]
theorem Real.arcsin_lt_pi_div_two {x : ℝ} :
arcsin x < Real.pi / 2 ↔ x < 1
source
@[simp]
theorem Real.neg_pi_div_two_lt_arcsin {x : ℝ} :
-(Real.pi / 2) < arcsin x ↔ -1 < x
source
@[simp]
theorem Real.arcsin_eq_pi_div_two {x : ℝ} :
arcsin x = Real.pi / 2 ↔ 1 ≤ x
source
@[simp]
theorem Real.pi_div_two_eq_arcsin {x : ℝ} :
Real.pi / 2 = arcsin x ↔ 1 ≤ x
source
@[simp]
theorem Real.pi_div_two_le_arcsin {x : ℝ} :
Real.pi / 2 ≤ arcsin x ↔ 1 ≤ x
source
@[simp]
theorem Real.arcsin_eq_neg_pi_div_two {x : ℝ} :
arcsin x = -(Real.pi / 2) ↔ x ≤ -1
source
@[simp]
theorem Real.neg_pi_div_two_eq_arcsin {x : ℝ} :
-(Real.pi / 2) = arcsin x ↔ x ≤ -1
source
@[simp]
theorem Real.arcsin_le_neg_pi_div_two {x : ℝ} :
arcsin x ≤ -(Real.pi / 2) ↔ x ≤ -1
source
@[simp]
theorem Real.pi_div_four_le_arcsin {x : ℝ} :
Real.pi / 4 ≤ arcsin x ↔ √2 / 2 ≤ x
source
theorem Real.mapsTo_sin_Ioo :
Set.MapsTo sin (Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)) (Set.Ioo (-1) 1)
source
def Real.sinPartialHomeomorph :
OpenPartialHomeomorph ℝ ℝ

`Real.sin` as an `OpenPartialHomeomorph` between `(-π / 2, π / 2)` and `(-1, 1)`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem Real.cos_arcsin_nonneg (x : ℝ) :
0 ≤ cos (arcsin x)
source
theorem Real.cos_arcsin (x : ℝ) :
cos (arcsin x) = √(1 - x ^ 2)
source
theorem Real.tan_arcsin (x : ℝ) :
tan (arcsin x) = x / √(1 - x ^ 2)
source
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

- Real.arccos x = Real.pi / 2 - Real.arcsin x

Instances For

source
theorem Real.arccos_eq_pi_div_two_sub_arcsin (x : ℝ) :
arccos x = Real.pi / 2 - arcsin x
source
theorem Real.arcsin_eq_pi_div_two_sub_arccos (x : ℝ) :
arcsin x = Real.pi / 2 - arccos x
source
theorem Real.arccos_le_pi (x : ℝ) :
arccos x ≤ Real.pi
source
theorem Real.arccos_nonneg (x : ℝ) :
0 ≤ arccos x
source
@[simp]
theorem Real.arccos_pos {x : ℝ} :
0 < arccos x ↔ x < 1
source
theorem Real.cos_arccos {x : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) :
cos (arccos x) = x
source
theorem Real.arccos_cos {x : ℝ} (hx₁ : 0 ≤ x) (hx₂ : x ≤ Real.pi) :
arccos (cos x) = x
source
theorem Real.arccos_eq_of_eq_cos {x y : ℝ} (hy₀ : 0 ≤ y) (hy₁ : y ≤ Real.pi) (hxy : x = cos y) :
arccos x = y
source
theorem Real.strictAntiOn_arccos :
StrictAntiOn arccos (Set.Icc (-1) 1)
source
theorem Real.arccos_lt_arccos {x y : ℝ} (hx : -1 ≤ x) (hlt : x < y) (hy : y ≤ 1) :
arccos y < arccos x
source
theorem Real.arccos_le_arccos {x y : ℝ} (hlt : x ≤ y) :
arccos y ≤ arccos x
source
theorem Real.antitone_arccos :
Antitone arccos
source
theorem Real.arccos_injOn :
Set.InjOn arccos (Set.Icc (-1) 1)
source
theorem Real.arccos_inj {x y : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) (hy₁ : -1 ≤ y) (hy₂ : y ≤ 1) :
arccos x = arccos y ↔ x = y
source
@[simp]
theorem Real.arccos_zero :
arccos 0 = Real.pi / 2
source
@[simp]
theorem Real.arccos_one :
arccos 1 = 0
source
@[simp]
theorem Real.arccos_neg_one :
arccos (-1) = Real.pi
source
@[simp]
theorem Real.arccos_eq_zero {x : ℝ} :
arccos x = 0 ↔ 1 ≤ x
source
@[simp]
theorem Real.arccos_eq_pi_div_two {x : ℝ} :
arccos x = Real.pi / 2 ↔ x = 0
source
@[simp]
theorem Real.arccos_eq_pi {x : ℝ} :
arccos x = Real.pi ↔ x ≤ -1
source
theorem Real.arccos_neg (x : ℝ) :
arccos (-x) = Real.pi - arccos x
source
theorem Real.arccos_of_one_le {x : ℝ} (hx : 1 ≤ x) :
arccos x = 0
source
theorem Real.arccos_of_le_neg_one {x : ℝ} (hx : x ≤ -1) :
arccos x = Real.pi
source
theorem Real.sin_arccos (x : ℝ) :
sin (arccos x) = √(1 - x ^ 2)
source
@[simp]
theorem Real.arccos_le_pi_div_two {x : ℝ} :
arccos x ≤ Real.pi / 2 ↔ 0 ≤ x
source
@[simp]
theorem Real.arccos_lt_pi_div_two {x : ℝ} :
arccos x < Real.pi / 2 ↔ 0 < x
source
@[simp]
theorem Real.arccos_le_pi_div_four {x : ℝ} :
arccos x ≤ Real.pi / 4 ↔ √2 / 2 ≤ x
source
theorem Real.continuous_arccos :
Continuous arccos
source
theorem Real.tan_arccos (x : ℝ) :
tan (arccos x) = √(1 - x ^ 2) / x
source
theorem Real.arccos_eq_arcsin {x : ℝ} (h : 0 ≤ x) :
arccos x = arcsin √(1 - x ^ 2)
source
theorem Real.arcsin_eq_arccos {x : ℝ} (h : 0 ≤ x) :
arcsin x = arccos √(1 - x ^ 2)

### Convenience dot notation lemmas #

source
theorem Filter.Tendsto.arcsin {α : Type u_1} {l : Filter α} {x : ℝ} {f : α → ℝ} (h : Tendsto f l (nhds x)) :
Tendsto (fun (x : α) => Real.arcsin (f x)) l (nhds (Real.arcsin x))
source
theorem Filter.Tendsto.arcsin_nhdsLE {α : Type u_1} {l : Filter α} {x : ℝ} {f : α → ℝ} (h : Tendsto f l (nhdsWithin x (Set.Iic x))) :
Tendsto (fun (x : α) => Real.arcsin (f x)) l (nhdsWithin (Real.arcsin x) (Set.Iic (Real.arcsin x)))
source
theorem Filter.Tendsto.arcsin_nhdsGE {α : Type u_1} {l : Filter α} {x : ℝ} {f : α → ℝ} (h : Tendsto f l (nhdsWithin x (Set.Ici x))) :
Tendsto (fun (x : α) => Real.arcsin (f x)) l (nhdsWithin (Real.arcsin x) (Set.Ici (Real.arcsin x)))
source
theorem Filter.Tendsto.arccos {α : Type u_1} {l : Filter α} {x : ℝ} {f : α → ℝ} (h : Tendsto f l (nhds x)) :
Tendsto (fun (x : α) => Real.arccos (f x)) l (nhds (Real.arccos x))
source
theorem Filter.Tendsto.arccos_nhdsLE {α : Type u_1} {l : Filter α} {x : ℝ} {f : α → ℝ} (h : Tendsto f l (nhdsWithin x (Set.Iic x))) :
Tendsto (fun (x : α) => Real.arccos (f x)) l (nhdsWithin (Real.arccos x) (Set.Ici (Real.arccos x)))
source
theorem Filter.Tendsto.arccos_nhdsGE {α : Type u_1} {l : Filter α} {x : ℝ} {f : α → ℝ} (h : Tendsto f l (nhdsWithin x (Set.Ici x))) :
Tendsto (fun (x : α) => Real.arccos (f x)) l (nhdsWithin (Real.arccos x) (Set.Iic (Real.arccos x)))
source
theorem ContinuousWithinAt.arcsin {X : Type u_1} [TopologicalSpace X] {f : X → ℝ} {s : Set X} {x : X} (h : ContinuousWithinAt f s x) :
ContinuousWithinAt (fun (x : X) => Real.arcsin (f x)) s x
source
theorem ContinuousWithinAt.arccos {X : Type u_1} [TopologicalSpace X] {f : X → ℝ} {s : Set X} {x : X} (h : ContinuousWithinAt f s x) :
ContinuousWithinAt (fun (x : X) => Real.arccos (f x)) s x
source
theorem ContinuousAt.arcsin {X : Type u_1} [TopologicalSpace X] {f : X → ℝ} {x : X} (h : ContinuousAt f x) :
ContinuousAt (fun (x : X) => Real.arcsin (f x)) x
source
theorem ContinuousAt.arccos {X : Type u_1} [TopologicalSpace X] {f : X → ℝ} {x : X} (h : ContinuousAt f x) :
ContinuousAt (fun (x : X) => Real.arccos (f x)) x
source
theorem ContinuousOn.arcsin {X : Type u_1} [TopologicalSpace X] {f : X → ℝ} {s : Set X} (h : ContinuousOn f s) :
ContinuousOn (fun (x : X) => Real.arcsin (f x)) s
source
theorem ContinuousOn.arccos {X : Type u_1} [TopologicalSpace X] {f : X → ℝ} {s : Set X} (h : ContinuousOn f s) :
ContinuousOn (fun (x : X) => Real.arccos (f x)) s
source
theorem Continuous.arcsin {X : Type u_1} [TopologicalSpace X] {f : X → ℝ} (h : Continuous f) :
Continuous fun (x : X) => Real.arcsin (f x)
source
theorem Continuous.arccos {X : Type u_1} [TopologicalSpace X] {f : X → ℝ} (h : Continuous f) :
Continuous fun (x : X) => Real.arccos (f x)