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, ∞)
.
Equations
Instances For
Convenience dot notation lemmas #
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))
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)))
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)))
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))
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)))
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)))
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
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
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
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
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
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
theorem
Continuous.arcsin
{X : Type u_1}
[TopologicalSpace X]
{f : X → ℝ}
(h : Continuous f)
:
Continuous fun (x : X) => Real.arcsin (f x)
theorem
Continuous.arccos
{X : Type u_1}
[TopologicalSpace X]
{f : X → ℝ}
(h : Continuous f)
:
Continuous fun (x : X) => Real.arccos (f x)