analysis.special_functions.trigonometric.inverse

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 = coe ∘ set.Icc_extend real.arcsin._proof_1 ⇑(real.sin_order_iso.symm)

source

theorem real.arcsin_mem_Icc (x : ℝ) :

real.arcsin x ∈ set.Icc (-(real.pi / 2)) (real.pi / 2)

source

@[simp]

theorem real.range_arcsin :

set.range real.arcsin = set.Icc (-(real.pi / 2)) (real.pi / 2)

source

theorem real.arcsin_le_pi_div_two (x : ℝ) :

real.arcsin x ≤ real.pi / 2

source

theorem real.neg_pi_div_two_le_arcsin (x : ℝ) :

-(real.pi / 2) ≤ real.arcsin x

source

theorem real.arcsin_proj_Icc (x : ℝ) :

real.arcsin ↑(set.proj_Icc (-1) 1 _ x) = real.arcsin x

source

theorem real.sin_arcsin' {x : ℝ} (hx : x ∈ set.Icc (-1) 1) :

real.sin (real.arcsin x) = x

source

theorem real.sin_arcsin {x : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) :

real.sin (real.arcsin x) = x

source

theorem real.arcsin_sin' {x : ℝ} (hx : x ∈ set.Icc (-(real.pi / 2)) (real.pi / 2)) :

real.arcsin (real.sin x) = x

source

theorem real.arcsin_sin {x : ℝ} (hx₁ : -(real.pi / 2) ≤ x) (hx₂ : x ≤ real.pi / 2) :

real.arcsin (real.sin x) = x

source

theorem real.strict_mono_on_arcsin :

strict_mono_on real.arcsin (set.Icc (-1) 1)

source

theorem real.monotone_arcsin :

monotone real.arcsin

source

theorem real.inj_on_arcsin :

set.inj_on real.arcsin (set.Icc (-1) 1)

source

theorem real.arcsin_inj {x y : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) (hy₁ : -1 ≤ y) (hy₂ : y ≤ 1) :

real.arcsin x = real.arcsin y ↔ x = y

source

@[continuity]

theorem real.continuous_arcsin :

continuous real.arcsin

source

theorem real.continuous_at_arcsin {x : ℝ} :

continuous_at real.arcsin x

source

theorem real.arcsin_eq_of_sin_eq {x y : ℝ} (h₁ : real.sin x = y) (h₂ : x ∈ set.Icc (-(real.pi / 2)) (real.pi / 2)) :

real.arcsin y = x

source

@[simp]

theorem real.arcsin_zero :

real.arcsin 0 = 0

source

@[simp]

theorem real.arcsin_one :

real.arcsin 1 = real.pi / 2

source

theorem real.arcsin_of_one_le {x : ℝ} (hx : 1 ≤ x) :

real.arcsin x = real.pi / 2

source

theorem real.arcsin_neg_one :

real.arcsin (-1) = -(real.pi / 2)

source

theorem real.arcsin_of_le_neg_one {x : ℝ} (hx : x ≤ -1) :

real.arcsin x = -(real.pi / 2)

source

@[simp]

theorem real.arcsin_neg (x : ℝ) :

real.arcsin (-x) = -real.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)) :

real.arcsin x ≤ y ↔ x ≤ real.sin y

source

theorem real.arcsin_le_iff_le_sin' {x y : ℝ} (hy : y ∈ set.Ico (-(real.pi / 2)) (real.pi / 2)) :

real.arcsin x ≤ y ↔ x ≤ real.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 ≤ real.arcsin y ↔ real.sin x ≤ y

source

theorem real.le_arcsin_iff_sin_le' {x y : ℝ} (hx : x ∈ set.Ioc (-(real.pi / 2)) (real.pi / 2)) :

x ≤ real.arcsin y ↔ real.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)) :

real.arcsin x < y ↔ x < real.sin y

source

theorem real.arcsin_lt_iff_lt_sin' {x y : ℝ} (hy : y ∈ set.Ioc (-(real.pi / 2)) (real.pi / 2)) :

real.arcsin x < y ↔ x < real.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 < real.arcsin y ↔ real.sin x < y

source

theorem real.lt_arcsin_iff_sin_lt' {x y : ℝ} (hx : x ∈ set.Ico (-(real.pi / 2)) (real.pi / 2)) :

x < real.arcsin y ↔ real.sin x < y

source

theorem real.arcsin_eq_iff_eq_sin {x y : ℝ} (hy : y ∈ set.Ioo (-(real.pi / 2)) (real.pi / 2)) :

real.arcsin x = y ↔ x = real.sin y

source

@[simp]

theorem real.arcsin_nonneg {x : ℝ} :

0 ≤ real.arcsin x ↔ 0 ≤ x

source

@[simp]

theorem real.arcsin_nonpos {x : ℝ} :

real.arcsin x ≤ 0 ↔ x ≤ 0

source

@[simp]

theorem real.arcsin_eq_zero_iff {x : ℝ} :

real.arcsin x = 0 ↔ x = 0

source

@[simp]

theorem real.zero_eq_arcsin_iff {x : ℝ} :

0 = real.arcsin x ↔ x = 0

source

@[simp]

theorem real.arcsin_pos {x : ℝ} :

0 < real.arcsin x ↔ 0 < x

source

@[simp]

theorem real.arcsin_lt_zero {x : ℝ} :

real.arcsin x < 0 ↔ x < 0

source

@[simp]

theorem real.arcsin_lt_pi_div_two {x : ℝ} :

real.arcsin x < real.pi / 2 ↔ x < 1

source

@[simp]

theorem real.neg_pi_div_two_lt_arcsin {x : ℝ} :

-(real.pi / 2) < real.arcsin x ↔ -1 < x

source

@[simp]

theorem real.arcsin_eq_pi_div_two {x : ℝ} :

real.arcsin x = real.pi / 2 ↔ 1 ≤ x

source

@[simp]

theorem real.pi_div_two_eq_arcsin {x : ℝ} :

real.pi / 2 = real.arcsin x ↔ 1 ≤ x

source

@[simp]

theorem real.pi_div_two_le_arcsin {x : ℝ} :

real.pi / 2 ≤ real.arcsin x ↔ 1 ≤ x

source

@[simp]

theorem real.arcsin_eq_neg_pi_div_two {x : ℝ} :

real.arcsin x = -(real.pi / 2) ↔ x ≤ -1

source

@[simp]

theorem real.neg_pi_div_two_eq_arcsin {x : ℝ} :

-(real.pi / 2) = real.arcsin x ↔ x ≤ -1

source

@[simp]

theorem real.arcsin_le_neg_pi_div_two {x : ℝ} :

real.arcsin x ≤ -(real.pi / 2) ↔ x ≤ -1

source

@[simp]

theorem real.pi_div_four_le_arcsin {x : ℝ} :

real.pi / 4 ≤ real.arcsin x ↔ √ 2 / 2 ≤ x

source

theorem real.maps_to_sin_Ioo :

set.maps_to real.sin (set.Ioo (-(real.pi / 2)) (real.pi / 2)) (set.Ioo (-1) 1)

source

@[simp]

noncomputable def real.sin_local_homeomorph :

local_homeomorph ℝ ℝ

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

Equations

real.sin_local_homeomorph = {to_local_equiv := {to_fun := real.sin, inv_fun := real.arcsin, source := set.Ioo (-(real.pi / 2)) (real.pi / 2), target := set.Ioo (-1) 1, map_source' := real.maps_to_sin_Ioo, map_target' := real.sin_local_homeomorph._proof_1, left_inv' := real.sin_local_homeomorph._proof_2, right_inv' := real.sin_local_homeomorph._proof_3}, open_source := real.sin_local_homeomorph._proof_4, open_target := real.sin_local_homeomorph._proof_5, continuous_to_fun := real.sin_local_homeomorph._proof_6, continuous_inv_fun := real.sin_local_homeomorph._proof_7}

source

theorem real.cos_arcsin_nonneg (x : ℝ) :

0 ≤ real.cos (real.arcsin x)

source

theorem real.cos_arcsin (x : ℝ) :

real.cos (real.arcsin x) = √ (1 - x ^ 2)

source

theorem real.tan_arcsin (x : ℝ) :

real.tan (real.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