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

• Real.arcsin = Subtype.val ∘ Set.IccExtend Real.arcsin.proof_2 ↑(OrderIso.symm Real.sinOrderIso)

theorem Real.arcsin_mem_Icc (x : ℝ) : Real.arcsin x ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2)

@[simp]

theorem Real.range_arcsin : Set.range Real.arcsin = Set.Icc (-(Real.pi / 2)) (Real.pi / 2)

theorem Real.arcsin_le_pi_div_two (x : ℝ) : Real.arcsin x ≤ Real.pi / 2

theorem Real.neg_pi_div_two_le_arcsin (x : ℝ) : -(Real.pi / 2) ≤ Real.arcsin x

theorem Real.arcsin_projIcc (x : ℝ) : Real.arcsin ↑(Set.projIcc (-1) 1 (_ : -1 ≤ 1) x) = Real.arcsin x

theorem Real.sin_arcsin' {x : ℝ} (hx : x ∈ Set.Icc (-1) 1) : Real.sin (Real.arcsin x) = x

theorem Real.sin_arcsin {x : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) : Real.sin (Real.arcsin x) = x

theorem Real.arcsin_sin' {x : ℝ} (hx : x ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) : Real.arcsin (Real.sin x) = x

theorem Real.arcsin_sin {x : ℝ} (hx₁ : -(Real.pi / 2) ≤ x) (hx₂ : x ≤ Real.pi / 2) : Real.arcsin (Real.sin x) = x

theorem Real.strictMonoOn_arcsin : StrictMonoOn Real.arcsin (Set.Icc (-1) 1)

theorem Real.monotone_arcsin : Monotone Real.arcsin

theorem Real.injOn_arcsin : Set.InjOn Real.arcsin (Set.Icc (-1) 1)

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

theorem Real.continuous_arcsin : Continuous Real.arcsin

theorem Real.continuousAt_arcsin {x : ℝ} : ContinuousAt Real.arcsin x

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

@[simp]

theorem Real.arcsin_zero : Real.arcsin 0 = 0

@[simp]

theorem Real.arcsin_one : Real.arcsin 1 = Real.pi / 2

theorem Real.arcsin_of_one_le {x : ℝ} (hx : 1 ≤ x) : Real.arcsin x = Real.pi / 2

theorem Real.arcsin_neg_one : Real.arcsin (-1) = -(Real.pi / 2)

theorem Real.arcsin_of_le_neg_one {x : ℝ} (hx : x ≤ -1) : Real.arcsin x = -(Real.pi / 2)

@[simp]

theorem Real.arcsin_neg (x : ℝ) : Real.arcsin (-x) = -Real.arcsin 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)) : Real.arcsin x ≤ y ↔ x ≤ Real.sin y

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

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

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

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

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

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

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

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

@[simp]

theorem Real.arcsin_nonneg {x : ℝ} : 0 ≤ Real.arcsin x ↔ 0 ≤ x

@[simp]

theorem Real.arcsin_nonpos {x : ℝ} : Real.arcsin x ≤ 0 ↔ x ≤ 0

@[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]

theorem Real.arcsin_lt_pi_div_two {x : ℝ} : Real.arcsin x < Real.pi / 2 ↔ x < 1

@[simp]

theorem Real.neg_pi_div_two_lt_arcsin {x : ℝ} : -(Real.pi / 2) < Real.arcsin x ↔ -1 < x

@[simp]

theorem Real.arcsin_eq_pi_div_two {x : ℝ} : Real.arcsin x = Real.pi / 2 ↔ 1 ≤ x

@[simp]

theorem Real.pi_div_two_eq_arcsin {x : ℝ} : Real.pi / 2 = Real.arcsin x ↔ 1 ≤ x

@[simp]

theorem Real.pi_div_two_le_arcsin {x : ℝ} : Real.pi / 2 ≤ Real.arcsin x ↔ 1 ≤ x

@[simp]

theorem Real.arcsin_eq_neg_pi_div_two {x : ℝ} : Real.arcsin x = -(Real.pi / 2) ↔ x ≤ -1

@[simp]

theorem Real.neg_pi_div_two_eq_arcsin {x : ℝ} : -(Real.pi / 2) = Real.arcsin x ↔ x ≤ -1

@[simp]

theorem Real.arcsin_le_neg_pi_div_two {x : ℝ} : Real.arcsin x ≤ -(Real.pi / 2) ↔ x ≤ -1

@[simp]

theorem Real.pi_div_four_le_arcsin {x : ℝ} : Real.pi / 4 ≤ Real.arcsin x ↔ Real.sqrt 2 / 2 ≤ x

theorem Real.mapsTo_sin_Ioo : Set.MapsTo Real.sin (Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)) (Set.Ioo (-1) 1)

def Real.sinLocalHomeomorph : LocalHomeomorph ℝ ℝ

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

Equations

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

theorem Real.cos_arcsin_nonneg (x : ℝ) : 0 ≤ Real.cos (Real.arcsin x)

theorem Real.cos_arcsin (x : ℝ) : Real.cos (Real.arcsin x) = Real.sqrt (1 - x ^ 2)

theorem Real.tan_arcsin (x : ℝ) : Real.tan (Real.arcsin x) = x / Real.sqrt (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

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

theorem Real.arccos_eq_pi_div_two_sub_arcsin (x : ℝ) : Real.arccos x = Real.pi / 2 - Real.arcsin x

theorem Real.arcsin_eq_pi_div_two_sub_arccos (x : ℝ) : Real.arcsin x = Real.pi / 2 - Real.arccos x

theorem Real.arccos_le_pi (x : ℝ) : Real.arccos x ≤ Real.pi

theorem Real.arccos_nonneg (x : ℝ) : 0 ≤ Real.arccos x

@[simp]

theorem Real.arccos_pos {x : ℝ} : 0 < Real.arccos x ↔ x < 1

theorem Real.cos_arccos {x : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) : Real.cos (Real.arccos x) = x

theorem Real.arccos_cos {x : ℝ} (hx₁ : 0 ≤ x) (hx₂ : x ≤ Real.pi) : Real.arccos (Real.cos x) = x

theorem Real.strictAntiOn_arccos : StrictAntiOn Real.arccos (Set.Icc (-1) 1)

theorem Real.arccos_injOn : Set.InjOn Real.arccos (Set.Icc (-1) 1)

theorem Real.arccos_inj {x : ℝ} {y : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) (hy₁ : -1 ≤ y) (hy₂ : y ≤ 1) : Real.arccos x = Real.arccos y ↔ x = y

@[simp]

theorem Real.arccos_zero : Real.arccos 0 = Real.pi / 2

@[simp]

theorem Real.arccos_one : Real.arccos 1 = 0

@[simp]

theorem Real.arccos_neg_one : Real.arccos (-1) = Real.pi

@[simp]

theorem Real.arccos_eq_zero {x : ℝ} : Real.arccos x = 0 ↔ 1 ≤ x

@[simp]

theorem Real.arccos_eq_pi_div_two {x : ℝ} : Real.arccos x = Real.pi / 2 ↔ x = 0

@[simp]

theorem Real.arccos_eq_pi {x : ℝ} : Real.arccos x = Real.pi ↔ x ≤ -1

theorem Real.arccos_neg (x : ℝ) : Real.arccos (-x) = Real.pi - Real.arccos x

theorem Real.arccos_of_one_le {x : ℝ} (hx : 1 ≤ x) : Real.arccos x = 0

theorem Real.arccos_of_le_neg_one {x : ℝ} (hx : x ≤ -1) : Real.arccos x = Real.pi

theorem Real.sin_arccos (x : ℝ) : Real.sin (Real.arccos x) = Real.sqrt (1 - x ^ 2)

@[simp]

theorem Real.arccos_le_pi_div_two {x : ℝ} : Real.arccos x ≤ Real.pi / 2 ↔ 0 ≤ x

@[simp]

theorem Real.arccos_lt_pi_div_two {x : ℝ} : Real.arccos x < Real.pi / 2 ↔ 0 < x

@[simp]

theorem Real.arccos_le_pi_div_four {x : ℝ} : Real.arccos x ≤ Real.pi / 4 ↔ Real.sqrt 2 / 2 ≤ x

theorem Real.continuous_arccos : Continuous Real.arccos

theorem Real.tan_arccos (x : ℝ) : Real.tan (Real.arccos x) = Real.sqrt (1 - x ^ 2) / x

theorem Real.arccos_eq_arcsin {x : ℝ} (h : 0 ≤ x) : Real.arccos x = Real.arcsin (Real.sqrt (1 - x ^ 2))

theorem Real.arcsin_eq_arccos {x : ℝ} (h : 0 ≤ x) : Real.arcsin x = Real.arccos (Real.sqrt (1 - x ^ 2))