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.
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, ∞)
.
Instances For
theorem
Real.arcsin_projIcc
(x : ℝ)
:
Real.arcsin ↑(Set.projIcc (-1) 1 (_ : -1 ≤ 1) x) = Real.arcsin x
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
Real.sin
as a LocalHomeomorph
between (-π / 2, π / 2)
and (-1, 1)
.
Instances For
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
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))