# mathlibdocumentation

analysis.special_functions.trigonometric

# Trigonometric functions #

## Main definitions #

This file contains the following definitions:

• π, arcsin, arccos, arctan
• argument of a complex number
• logarithm on complex numbers

## Main statements #

Many basic inequalities on trigonometric functions are established.

The continuity and differentiability of the usual trigonometric functions are proved, and their derivatives are computed.

• `polynomial.chebyshev.T_complex_cos`: the `n`-th Chebyshev polynomial evaluates on `complex.cos θ` to the value `n * complex.cos θ`.

## Tags #

log, sin, cos, tan, arcsin, arccos, arctan, angle, argument

The complex sine function is everywhere strictly differentiable, with the derivative `cos x`.

theorem complex.has_deriv_at_sin (x : ) :

The complex sine function is everywhere differentiable, with the derivative `cos x`.

@[simp]

The complex cosine function is everywhere strictly differentiable, with the derivative `-sin x`.

theorem complex.has_deriv_at_cos (x : ) :

The complex cosine function is everywhere differentiable, with the derivative `-sin x`.

theorem complex.deriv_cos {x : } :
@[simp]
theorem complex.deriv_cos'  :
= λ (x : ),

The complex hyperbolic sine function is everywhere strictly differentiable, with the derivative `cosh x`.

theorem complex.has_deriv_at_sinh (x : ) :

The complex hyperbolic sine function is everywhere differentiable, with the derivative `cosh x`.

@[simp]

The complex hyperbolic cosine function is everywhere strictly differentiable, with the derivative `sinh x`.

theorem complex.has_deriv_at_cosh (x : ) :

The complex hyperbolic cosine function is everywhere differentiable, with the derivative `sinh x`.

@[simp]

### Simp lemmas for derivatives of `λ x, complex.cos (f x)` etc., `f : ℂ → ℂ`#

#### `complex.cos`#

theorem has_strict_deriv_at.ccos {f : } {f' x : } (hf : x) :
has_strict_deriv_at (λ (x : ), complex.cos (f x)) ((-complex.sin (f x)) * f') x
theorem has_deriv_at.ccos {f : } {f' x : } (hf : f' x) :
has_deriv_at (λ (x : ), complex.cos (f x)) ((-complex.sin (f x)) * f') x
theorem has_deriv_within_at.ccos {f : } {f' x : } {s : set } (hf : s x) :
has_deriv_within_at (λ (x : ), complex.cos (f x)) ((-complex.sin (f x)) * f') s x
theorem deriv_within_ccos {f : } {x : } {s : set } (hf : x) (hxs : x) :
deriv_within (λ (x : ), complex.cos (f x)) s x = (-complex.sin (f x)) * s x
@[simp]
theorem deriv_ccos {f : } {x : } (hc : x) :
deriv (λ (x : ), complex.cos (f x)) x = (-complex.sin (f x)) * x

#### `complex.sin`#

theorem has_strict_deriv_at.csin {f : } {f' x : } (hf : x) :
has_strict_deriv_at (λ (x : ), complex.sin (f x)) ((complex.cos (f x)) * f') x
theorem has_deriv_at.csin {f : } {f' x : } (hf : f' x) :
has_deriv_at (λ (x : ), complex.sin (f x)) ((complex.cos (f x)) * f') x
theorem has_deriv_within_at.csin {f : } {f' x : } {s : set } (hf : s x) :
has_deriv_within_at (λ (x : ), complex.sin (f x)) ((complex.cos (f x)) * f') s x
theorem deriv_within_csin {f : } {x : } {s : set } (hf : x) (hxs : x) :
deriv_within (λ (x : ), complex.sin (f x)) s x = (complex.cos (f x)) * s x
@[simp]
theorem deriv_csin {f : } {x : } (hc : x) :
deriv (λ (x : ), complex.sin (f x)) x = (complex.cos (f x)) * x

#### `complex.cosh`#

theorem has_strict_deriv_at.ccosh {f : } {f' x : } (hf : x) :
has_strict_deriv_at (λ (x : ), complex.cosh (f x)) ((complex.sinh (f x)) * f') x
theorem has_deriv_at.ccosh {f : } {f' x : } (hf : f' x) :
has_deriv_at (λ (x : ), complex.cosh (f x)) ((complex.sinh (f x)) * f') x
theorem has_deriv_within_at.ccosh {f : } {f' x : } {s : set } (hf : s x) :
has_deriv_within_at (λ (x : ), complex.cosh (f x)) ((complex.sinh (f x)) * f') s x
theorem deriv_within_ccosh {f : } {x : } {s : set } (hf : x) (hxs : x) :
deriv_within (λ (x : ), complex.cosh (f x)) s x = (complex.sinh (f x)) * s x
@[simp]
theorem deriv_ccosh {f : } {x : } (hc : x) :
deriv (λ (x : ), complex.cosh (f x)) x = (complex.sinh (f x)) * x

#### `complex.sinh`#

theorem has_strict_deriv_at.csinh {f : } {f' x : } (hf : x) :
has_strict_deriv_at (λ (x : ), complex.sinh (f x)) ((complex.cosh (f x)) * f') x
theorem has_deriv_at.csinh {f : } {f' x : } (hf : f' x) :
has_deriv_at (λ (x : ), complex.sinh (f x)) ((complex.cosh (f x)) * f') x
theorem has_deriv_within_at.csinh {f : } {f' x : } {s : set } (hf : s x) :
has_deriv_within_at (λ (x : ), complex.sinh (f x)) ((complex.cosh (f x)) * f') s x
theorem deriv_within_csinh {f : } {x : } {s : set } (hf : x) (hxs : x) :
deriv_within (λ (x : ), complex.sinh (f x)) s x = (complex.cosh (f x)) * s x
@[simp]
theorem deriv_csinh {f : } {x : } (hc : x) :
deriv (λ (x : ), complex.sinh (f x)) x = (complex.cosh (f x)) * x

### Simp lemmas for derivatives of `λ x, complex.cos (f x)` etc., `f : E → ℂ`#

#### `complex.cos`#

theorem has_strict_fderiv_at.ccos {E : Type u_1} [normed_group E] [ E] {f : E → } {f' : E →L[] } {x : E} (hf : x) :
has_strict_fderiv_at (λ (x : E), complex.cos (f x)) (-complex.sin (f x) f') x
theorem has_fderiv_at.ccos {E : Type u_1} [normed_group E] [ E] {f : E → } {f' : E →L[] } {x : E} (hf : f' x) :
has_fderiv_at (λ (x : E), complex.cos (f x)) (-complex.sin (f x) f') x
theorem has_fderiv_within_at.ccos {E : Type u_1} [normed_group E] [ E] {f : E → } {f' : E →L[] } {x : E} {s : set E} (hf : s x) :
has_fderiv_within_at (λ (x : E), complex.cos (f x)) (-complex.sin (f x) f') s x
theorem differentiable_within_at.ccos {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {s : set E} (hf : x) :
(λ (x : E), complex.cos (f x)) s x
@[simp]
theorem differentiable_at.ccos {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} (hc : x) :
(λ (x : E), complex.cos (f x)) x
theorem differentiable_on.ccos {E : Type u_1} [normed_group E] [ E] {f : E → } {s : set E} (hc : s) :
(λ (x : E), complex.cos (f x)) s
@[simp]
theorem differentiable.ccos {E : Type u_1} [normed_group E] [ E] {f : E → } (hc : f) :
(λ (x : E), complex.cos (f x))
theorem fderiv_within_ccos {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {s : set E} (hf : x) (hxs : x) :
(λ (x : E), complex.cos (f x)) s x = -complex.sin (f x) s x
@[simp]
theorem fderiv_ccos {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} (hc : x) :
(λ (x : E), complex.cos (f x)) x = -complex.sin (f x) f x
theorem times_cont_diff.ccos {E : Type u_1} [normed_group E] [ E] {f : E → } {n : with_top } (h : f) :
(λ (x : E), complex.cos (f x))
theorem times_cont_diff_at.ccos {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {n : with_top } (hf : x) :
(λ (x : E), complex.cos (f x)) x
theorem times_cont_diff_on.ccos {E : Type u_1} [normed_group E] [ E] {f : E → } {s : set E} {n : with_top } (hf : s) :
(λ (x : E), complex.cos (f x)) s
theorem times_cont_diff_within_at.ccos {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : x) :
(λ (x : E), complex.cos (f x)) s x

#### `complex.sin`#

theorem has_strict_fderiv_at.csin {E : Type u_1} [normed_group E] [ E] {f : E → } {f' : E →L[] } {x : E} (hf : x) :
has_strict_fderiv_at (λ (x : E), complex.sin (f x)) (complex.cos (f x) f') x
theorem has_fderiv_at.csin {E : Type u_1} [normed_group E] [ E] {f : E → } {f' : E →L[] } {x : E} (hf : f' x) :
has_fderiv_at (λ (x : E), complex.sin (f x)) (complex.cos (f x) f') x
theorem has_fderiv_within_at.csin {E : Type u_1} [normed_group E] [ E] {f : E → } {f' : E →L[] } {x : E} {s : set E} (hf : s x) :
has_fderiv_within_at (λ (x : E), complex.sin (f x)) (complex.cos (f x) f') s x
theorem differentiable_within_at.csin {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {s : set E} (hf : x) :
(λ (x : E), complex.sin (f x)) s x
@[simp]
theorem differentiable_at.csin {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} (hc : x) :
(λ (x : E), complex.sin (f x)) x
theorem differentiable_on.csin {E : Type u_1} [normed_group E] [ E] {f : E → } {s : set E} (hc : s) :
(λ (x : E), complex.sin (f x)) s
@[simp]
theorem differentiable.csin {E : Type u_1} [normed_group E] [ E] {f : E → } (hc : f) :
(λ (x : E), complex.sin (f x))
theorem fderiv_within_csin {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {s : set E} (hf : x) (hxs : x) :
(λ (x : E), complex.sin (f x)) s x = complex.cos (f x) s x
@[simp]
theorem fderiv_csin {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} (hc : x) :
(λ (x : E), complex.sin (f x)) x = complex.cos (f x) f x
theorem times_cont_diff.csin {E : Type u_1} [normed_group E] [ E] {f : E → } {n : with_top } (h : f) :
(λ (x : E), complex.sin (f x))
theorem times_cont_diff_at.csin {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {n : with_top } (hf : x) :
(λ (x : E), complex.sin (f x)) x
theorem times_cont_diff_on.csin {E : Type u_1} [normed_group E] [ E] {f : E → } {s : set E} {n : with_top } (hf : s) :
(λ (x : E), complex.sin (f x)) s
theorem times_cont_diff_within_at.csin {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : x) :
(λ (x : E), complex.sin (f x)) s x

#### `complex.cosh`#

theorem has_strict_fderiv_at.ccosh {E : Type u_1} [normed_group E] [ E] {f : E → } {f' : E →L[] } {x : E} (hf : x) :
has_strict_fderiv_at (λ (x : E), complex.cosh (f x)) (complex.sinh (f x) f') x
theorem has_fderiv_at.ccosh {E : Type u_1} [normed_group E] [ E] {f : E → } {f' : E →L[] } {x : E} (hf : f' x) :
has_fderiv_at (λ (x : E), complex.cosh (f x)) (complex.sinh (f x) f') x
theorem has_fderiv_within_at.ccosh {E : Type u_1} [normed_group E] [ E] {f : E → } {f' : E →L[] } {x : E} {s : set E} (hf : s x) :
has_fderiv_within_at (λ (x : E), complex.cosh (f x)) (complex.sinh (f x) f') s x
theorem differentiable_within_at.ccosh {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {s : set E} (hf : x) :
(λ (x : E), complex.cosh (f x)) s x
@[simp]
theorem differentiable_at.ccosh {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} (hc : x) :
(λ (x : E), complex.cosh (f x)) x
theorem differentiable_on.ccosh {E : Type u_1} [normed_group E] [ E] {f : E → } {s : set E} (hc : s) :
(λ (x : E), complex.cosh (f x)) s
@[simp]
theorem differentiable.ccosh {E : Type u_1} [normed_group E] [ E] {f : E → } (hc : f) :
(λ (x : E), complex.cosh (f x))
theorem fderiv_within_ccosh {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {s : set E} (hf : x) (hxs : x) :
(λ (x : E), complex.cosh (f x)) s x = complex.sinh (f x) s x
@[simp]
theorem fderiv_ccosh {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} (hc : x) :
(λ (x : E), complex.cosh (f x)) x = complex.sinh (f x) f x
theorem times_cont_diff.ccosh {E : Type u_1} [normed_group E] [ E] {f : E → } {n : with_top } (h : f) :
(λ (x : E), complex.cosh (f x))
theorem times_cont_diff_at.ccosh {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {n : with_top } (hf : x) :
(λ (x : E), complex.cosh (f x)) x
theorem times_cont_diff_on.ccosh {E : Type u_1} [normed_group E] [ E] {f : E → } {s : set E} {n : with_top } (hf : s) :
(λ (x : E), complex.cosh (f x)) s
theorem times_cont_diff_within_at.ccosh {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : x) :
(λ (x : E), complex.cosh (f x)) s x

#### `complex.sinh`#

theorem has_strict_fderiv_at.csinh {E : Type u_1} [normed_group E] [ E] {f : E → } {f' : E →L[] } {x : E} (hf : x) :
has_strict_fderiv_at (λ (x : E), complex.sinh (f x)) (complex.cosh (f x) f') x
theorem has_fderiv_at.csinh {E : Type u_1} [normed_group E] [ E] {f : E → } {f' : E →L[] } {x : E} (hf : f' x) :
has_fderiv_at (λ (x : E), complex.sinh (f x)) (complex.cosh (f x) f') x
theorem has_fderiv_within_at.csinh {E : Type u_1} [normed_group E] [ E] {f : E → } {f' : E →L[] } {x : E} {s : set E} (hf : s x) :
has_fderiv_within_at (λ (x : E), complex.sinh (f x)) (complex.cosh (f x) f') s x
theorem differentiable_within_at.csinh {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {s : set E} (hf : x) :
(λ (x : E), complex.sinh (f x)) s x
@[simp]
theorem differentiable_at.csinh {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} (hc : x) :
(λ (x : E), complex.sinh (f x)) x
theorem differentiable_on.csinh {E : Type u_1} [normed_group E] [ E] {f : E → } {s : set E} (hc : s) :
(λ (x : E), complex.sinh (f x)) s
@[simp]
theorem differentiable.csinh {E : Type u_1} [normed_group E] [ E] {f : E → } (hc : f) :
(λ (x : E), complex.sinh (f x))
theorem fderiv_within_csinh {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {s : set E} (hf : x) (hxs : x) :
(λ (x : E), complex.sinh (f x)) s x = complex.cosh (f x) s x
@[simp]
theorem fderiv_csinh {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} (hc : x) :
(λ (x : E), complex.sinh (f x)) x = complex.cosh (f x) f x
theorem times_cont_diff.csinh {E : Type u_1} [normed_group E] [ E] {f : E → } {n : with_top } (h : f) :
(λ (x : E), complex.sinh (f x))
theorem times_cont_diff_at.csinh {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {n : with_top } (hf : x) :
(λ (x : E), complex.sinh (f x)) x
theorem times_cont_diff_on.csinh {E : Type u_1} [normed_group E] [ E] {f : E → } {s : set E} {n : with_top } (hf : s) :
(λ (x : E), complex.sinh (f x)) s
theorem times_cont_diff_within_at.csinh {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : x) :
(λ (x : E), complex.sinh (f x)) s x
theorem real.has_deriv_at_sin (x : ) :
x
@[simp]
theorem real.deriv_sin  :
theorem real.has_deriv_at_cos (x : ) :
theorem real.deriv_cos {x : } :
@[simp]
theorem real.deriv_cos'  :
= λ (x : ),
theorem real.has_deriv_at_sinh (x : ) :
@[simp]
theorem real.deriv_sinh  :
theorem real.has_deriv_at_cosh (x : ) :
@[simp]
theorem real.deriv_cosh  :

`sinh` is strictly monotone.

### Simp lemmas for derivatives of `λ x, real.cos (f x)` etc., `f : ℝ → ℝ`#

#### `real.cos`#

theorem has_strict_deriv_at.cos {f : } {f' x : } (hf : x) :
has_strict_deriv_at (λ (x : ), real.cos (f x)) ((-real.sin (f x)) * f') x
theorem has_deriv_at.cos {f : } {f' x : } (hf : f' x) :
has_deriv_at (λ (x : ), real.cos (f x)) ((-real.sin (f x)) * f') x
theorem has_deriv_within_at.cos {f : } {f' x : } {s : set } (hf : s x) :
has_deriv_within_at (λ (x : ), real.cos (f x)) ((-real.sin (f x)) * f') s x
theorem deriv_within_cos {f : } {x : } {s : set } (hf : x) (hxs : x) :
deriv_within (λ (x : ), real.cos (f x)) s x = (-real.sin (f x)) * s x
@[simp]
theorem deriv_cos {f : } {x : } (hc : x) :
deriv (λ (x : ), real.cos (f x)) x = (-real.sin (f x)) * x

#### `real.sin`#

theorem has_strict_deriv_at.sin {f : } {f' x : } (hf : x) :
has_strict_deriv_at (λ (x : ), real.sin (f x)) ((real.cos (f x)) * f') x
theorem has_deriv_at.sin {f : } {f' x : } (hf : f' x) :
has_deriv_at (λ (x : ), real.sin (f x)) ((real.cos (f x)) * f') x
theorem has_deriv_within_at.sin {f : } {f' x : } {s : set } (hf : s x) :
has_deriv_within_at (λ (x : ), real.sin (f x)) ((real.cos (f x)) * f') s x
theorem deriv_within_sin {f : } {x : } {s : set } (hf : x) (hxs : x) :
deriv_within (λ (x : ), real.sin (f x)) s x = (real.cos (f x)) * s x
@[simp]
theorem deriv_sin {f : } {x : } (hc : x) :
deriv (λ (x : ), real.sin (f x)) x = (real.cos (f x)) * x

#### `real.cosh`#

theorem has_strict_deriv_at.cosh {f : } {f' x : } (hf : x) :
has_strict_deriv_at (λ (x : ), real.cosh (f x)) ((real.sinh (f x)) * f') x
theorem has_deriv_at.cosh {f : } {f' x : } (hf : f' x) :
has_deriv_at (λ (x : ), real.cosh (f x)) ((real.sinh (f x)) * f') x
theorem has_deriv_within_at.cosh {f : } {f' x : } {s : set } (hf : s x) :
has_deriv_within_at (λ (x : ), real.cosh (f x)) ((real.sinh (f x)) * f') s x
theorem deriv_within_cosh {f : } {x : } {s : set } (hf : x) (hxs : x) :
deriv_within (λ (x : ), real.cosh (f x)) s x = (real.sinh (f x)) * s x
@[simp]
theorem deriv_cosh {f : } {x : } (hc : x) :
deriv (λ (x : ), real.cosh (f x)) x = (real.sinh (f x)) * x

#### `real.sinh`#

theorem has_strict_deriv_at.sinh {f : } {f' x : } (hf : x) :
has_strict_deriv_at (λ (x : ), real.sinh (f x)) ((real.cosh (f x)) * f') x
theorem has_deriv_at.sinh {f : } {f' x : } (hf : f' x) :
has_deriv_at (λ (x : ), real.sinh (f x)) ((real.cosh (f x)) * f') x
theorem has_deriv_within_at.sinh {f : } {f' x : } {s : set } (hf : s x) :
has_deriv_within_at (λ (x : ), real.sinh (f x)) ((real.cosh (f x)) * f') s x
theorem deriv_within_sinh {f : } {x : } {s : set } (hf : x) (hxs : x) :
deriv_within (λ (x : ), real.sinh (f x)) s x = (real.cosh (f x)) * s x
@[simp]
theorem deriv_sinh {f : } {x : } (hc : x) :
deriv (λ (x : ), real.sinh (f x)) x = (real.cosh (f x)) * x

### Simp lemmas for derivatives of `λ x, real.cos (f x)` etc., `f : E → ℝ`#

#### `real.cos`#

theorem has_strict_fderiv_at.cos {E : Type u_1} [normed_group E] [ E] {f : E → } {f' : E →L[] } {x : E} (hf : x) :
has_strict_fderiv_at (λ (x : E), real.cos (f x)) (-real.sin (f x) f') x
theorem has_fderiv_at.cos {E : Type u_1} [normed_group E] [ E] {f : E → } {f' : E →L[] } {x : E} (hf : f' x) :
has_fderiv_at (λ (x : E), real.cos (f x)) (-real.sin (f x) f') x
theorem has_fderiv_within_at.cos {E : Type u_1} [normed_group E] [ E] {f : E → } {f' : E →L[] } {x : E} {s : set E} (hf : s x) :
has_fderiv_within_at (λ (x : E), real.cos (f x)) (-real.sin (f x) f') s x
theorem differentiable_within_at.cos {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {s : set E} (hf : x) :
(λ (x : E), real.cos (f x)) s x
@[simp]
theorem differentiable_at.cos {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} (hc : x) :
(λ (x : E), real.cos (f x)) x
theorem differentiable_on.cos {E : Type u_1} [normed_group E] [ E] {f : E → } {s : set E} (hc : s) :
(λ (x : E), real.cos (f x)) s
@[simp]
theorem differentiable.cos {E : Type u_1} [normed_group E] [ E] {f : E → } (hc : f) :
(λ (x : E), real.cos (f x))
theorem fderiv_within_cos {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {s : set E} (hf : x) (hxs : x) :
(λ (x : E), real.cos (f x)) s x = -real.sin (f x) s x
@[simp]
theorem fderiv_cos {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} (hc : x) :
(λ (x : E), real.cos (f x)) x = -real.sin (f x) f x
theorem times_cont_diff.cos {E : Type u_1} [normed_group E] [ E] {f : E → } {n : with_top } (h : f) :
(λ (x : E), real.cos (f x))
theorem times_cont_diff_at.cos {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {n : with_top } (hf : x) :
(λ (x : E), real.cos (f x)) x
theorem times_cont_diff_on.cos {E : Type u_1} [normed_group E] [ E] {f : E → } {s : set E} {n : with_top } (hf : s) :
(λ (x : E), real.cos (f x)) s
theorem times_cont_diff_within_at.cos {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : x) :
(λ (x : E), real.cos (f x)) s x

#### `real.sin`#

theorem has_strict_fderiv_at.sin {E : Type u_1} [normed_group E] [ E] {f : E → } {f' : E →L[] } {x : E} (hf : x) :
has_strict_fderiv_at (λ (x : E), real.sin (f x)) (real.cos (f x) f') x
theorem has_fderiv_at.sin {E : Type u_1} [normed_group E] [ E] {f : E → } {f' : E →L[] } {x : E} (hf : f' x) :
has_fderiv_at (λ (x : E), real.sin (f x)) (real.cos (f x) f') x
theorem has_fderiv_within_at.sin {E : Type u_1} [normed_group E] [ E] {f : E → } {f' : E →L[] } {x : E} {s : set E} (hf : s x) :
has_fderiv_within_at (λ (x : E), real.sin (f x)) (real.cos (f x) f') s x
theorem differentiable_within_at.sin {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {s : set E} (hf : x) :
(λ (x : E), real.sin (f x)) s x
@[simp]
theorem differentiable_at.sin {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} (hc : x) :
(λ (x : E), real.sin (f x)) x
theorem differentiable_on.sin {E : Type u_1} [normed_group E] [ E] {f : E → } {s : set E} (hc : s) :
(λ (x : E), real.sin (f x)) s
@[simp]
theorem differentiable.sin {E : Type u_1} [normed_group E] [ E] {f : E → } (hc : f) :
(λ (x : E), real.sin (f x))
theorem fderiv_within_sin {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {s : set E} (hf : x) (hxs : x) :
(λ (x : E), real.sin (f x)) s x = real.cos (f x) s x
@[simp]
theorem fderiv_sin {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} (hc : x) :
(λ (x : E), real.sin (f x)) x = real.cos (f x) f x
theorem times_cont_diff.sin {E : Type u_1} [normed_group E] [ E] {f : E → } {n : with_top } (h : f) :
(λ (x : E), real.sin (f x))
theorem times_cont_diff_at.sin {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {n : with_top } (hf : x) :
(λ (x : E), real.sin (f x)) x
theorem times_cont_diff_on.sin {E : Type u_1} [normed_group E] [ E] {f : E → } {s : set E} {n : with_top } (hf : s) :
(λ (x : E), real.sin (f x)) s
theorem times_cont_diff_within_at.sin {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : x) :
(λ (x : E), real.sin (f x)) s x

#### `real.cosh`#

theorem has_strict_fderiv_at.cosh {E : Type u_1} [normed_group E] [ E] {f : E → } {f' : E →L[] } {x : E} (hf : x) :
has_strict_fderiv_at (λ (x : E), real.cosh (f x)) (real.sinh (f x) f') x
theorem has_fderiv_at.cosh {E : Type u_1} [normed_group E] [ E] {f : E → } {f' : E →L[] } {x : E} (hf : f' x) :
has_fderiv_at (λ (x : E), real.cosh (f x)) (real.sinh (f x) f') x
theorem has_fderiv_within_at.cosh {E : Type u_1} [normed_group E] [ E] {f : E → } {f' : E →L[] } {x : E} {s : set E} (hf : s x) :
has_fderiv_within_at (λ (x : E), real.cosh (f x)) (real.sinh (f x) f') s x
theorem differentiable_within_at.cosh {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {s : set E} (hf : x) :
(λ (x : E), real.cosh (f x)) s x
@[simp]
theorem differentiable_at.cosh {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} (hc : x) :
(λ (x : E), real.cosh (f x)) x
theorem differentiable_on.cosh {E : Type u_1} [normed_group E] [ E] {f : E → } {s : set E} (hc : s) :
(λ (x : E), real.cosh (f x)) s
@[simp]
theorem differentiable.cosh {E : Type u_1} [normed_group E] [ E] {f : E → } (hc : f) :
(λ (x : E), real.cosh (f x))
theorem fderiv_within_cosh {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {s : set E} (hf : x) (hxs : x) :
(λ (x : E), real.cosh (f x)) s x = real.sinh (f x) s x
@[simp]
theorem fderiv_cosh {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} (hc : x) :
(λ (x : E), real.cosh (f x)) x = real.sinh (f x) f x
theorem times_cont_diff.cosh {E : Type u_1} [normed_group E] [ E] {f : E → } {n : with_top } (h : f) :
(λ (x : E), real.cosh (f x))
theorem times_cont_diff_at.cosh {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {n : with_top } (hf : x) :
(λ (x : E), real.cosh (f x)) x
theorem times_cont_diff_on.cosh {E : Type u_1} [normed_group E] [ E] {f : E → } {s : set E} {n : with_top } (hf : s) :
(λ (x : E), real.cosh (f x)) s
theorem times_cont_diff_within_at.cosh {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : x) :
(λ (x : E), real.cosh (f x)) s x

#### `real.sinh`#

theorem has_strict_fderiv_at.sinh {E : Type u_1} [normed_group E] [ E] {f : E → } {f' : E →L[] } {x : E} (hf : x) :
has_strict_fderiv_at (λ (x : E), real.sinh (f x)) (real.cosh (f x) f') x
theorem has_fderiv_at.sinh {E : Type u_1} [normed_group E] [ E] {f : E → } {f' : E →L[] } {x : E} (hf : f' x) :
has_fderiv_at (λ (x : E), real.sinh (f x)) (real.cosh (f x) f') x
theorem has_fderiv_within_at.sinh {E : Type u_1} [normed_group E] [ E] {f : E → } {f' : E →L[] } {x : E} {s : set E} (hf : s x) :
has_fderiv_within_at (λ (x : E), real.sinh (f x)) (real.cosh (f x) f') s x
theorem differentiable_within_at.sinh {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {s : set E} (hf : x) :
(λ (x : E), real.sinh (f x)) s x
@[simp]
theorem differentiable_at.sinh {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} (hc : x) :
(λ (x : E), real.sinh (f x)) x
theorem differentiable_on.sinh {E : Type u_1} [normed_group E] [ E] {f : E → } {s : set E} (hc : s) :
(λ (x : E), real.sinh (f x)) s
@[simp]
theorem differentiable.sinh {E : Type u_1} [normed_group E] [ E] {f : E → } (hc : f) :
(λ (x : E), real.sinh (f x))
theorem fderiv_within_sinh {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {s : set E} (hf : x) (hxs : x) :
(λ (x : E), real.sinh (f x)) s x = real.cosh (f x) s x
@[simp]
theorem fderiv_sinh {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} (hc : x) :
(λ (x : E), real.sinh (f x)) x = real.cosh (f x) f x
theorem times_cont_diff.sinh {E : Type u_1} [normed_group E] [ E] {f : E → } {n : with_top } (h : f) :
(λ (x : E), real.sinh (f x))
theorem times_cont_diff_at.sinh {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {n : with_top } (hf : x) :
(λ (x : E), real.sinh (f x)) x
theorem times_cont_diff_on.sinh {E : Type u_1} [normed_group E] [ E] {f : E → } {s : set E} {n : with_top } (hf : s) :
(λ (x : E), real.sinh (f x)) s
theorem times_cont_diff_within_at.sinh {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : x) :
(λ (x : E), real.sinh (f x)) s x
def real.pi  :

The number π = 3.14159265... Defined here using choice as twice a zero of cos in [1,2], from which one can derive all its properties. For explicit bounds on π, see `data.real.pi`.

Equations
@[simp]
theorem real.cos_pi_div_two  :
real.cos (π / 2) = 0
theorem real.two_le_pi  :
theorem real.pi_le_four  :
theorem real.pi_pos  :
0 < π
theorem real.pi_ne_zero  :
theorem real.pi_div_two_pos  :
0 < π / 2
theorem real.two_pi_pos  :
0 < 2 * π
def nnreal.pi  :

`π` considered as a nonnegative real.

Equations
@[simp]
theorem nnreal.coe_real_pi  :
theorem nnreal.pi_pos  :
@[simp]
theorem real.sin_pi  :
@[simp]
theorem real.cos_pi  :
= -1
@[simp]
theorem real.sin_two_pi  :
real.sin (2 * π) = 0
@[simp]
theorem real.cos_two_pi  :
real.cos (2 * π) = 1
theorem real.sin_add_pi (x : ) :
real.sin (x + π) =
theorem real.sin_add_two_pi (x : ) :
real.sin (x + 2 * π) =
theorem real.sin_sub_pi (x : ) :
real.sin (x - π) =
theorem real.sin_sub_two_pi (x : ) :
real.sin (x - 2 * π) =
theorem real.sin_pi_sub (x : ) :
real.sin (π - x) =
theorem real.sin_two_pi_sub (x : ) :
real.sin (2 * π - x) =
theorem real.sin_nat_mul_pi (n : ) :
real.sin ((n) * π) = 0
theorem real.sin_int_mul_pi (n : ) :
real.sin ((n) * π) = 0
theorem real.sin_add_nat_mul_two_pi (x : ) (n : ) :
real.sin (x + (n) * 2 * π) =
theorem real.sin_add_int_mul_two_pi (x : ) (n : ) :
real.sin (x + (n) * 2 * π) =
theorem real.sin_sub_nat_mul_two_pi (x : ) (n : ) :
real.sin (x - (n) * 2 * π) =
theorem real.sin_sub_int_mul_two_pi (x : ) (n : ) :
real.sin (x - (n) * 2 * π) =
theorem real.sin_nat_mul_two_pi_sub (x : ) (n : ) :
real.sin ((n) * 2 * π - x) =
theorem real.sin_int_mul_two_pi_sub (x : ) (n : ) :
real.sin ((n) * 2 * π - x) =
theorem real.cos_add_pi (x : ) :
real.cos (x + π) =
theorem real.cos_add_two_pi (x : ) :
real.cos (x + 2 * π) =
theorem real.cos_sub_pi (x : ) :
real.cos (x - π) =
theorem real.cos_sub_two_pi (x : ) :
real.cos (x - 2 * π) =
theorem real.cos_pi_sub (x : ) :
real.cos (π - x) =
theorem real.cos_two_pi_sub (x : ) :
real.cos (2 * π - x) =
theorem real.cos_nat_mul_two_pi (n : ) :
real.cos ((n) * 2 * π) = 1
theorem real.cos_int_mul_two_pi (n : ) :
real.cos ((n) * 2 * π) = 1
theorem real.cos_add_nat_mul_two_pi (x : ) (n : ) :
real.cos (x + (n) * 2 * π) =
theorem real.cos_add_int_mul_two_pi (x : ) (n : ) :
real.cos (x + (n) * 2 * π) =
theorem real.cos_sub_nat_mul_two_pi (x : ) (n : ) :
real.cos (x - (n) * 2 * π) =
theorem real.cos_sub_int_mul_two_pi (x : ) (n : ) :
real.cos (x - (n) * 2 * π) =
theorem real.cos_nat_mul_two_pi_sub (x : ) (n : ) :
real.cos ((n) * 2 * π - x) =
theorem real.cos_int_mul_two_pi_sub (x : ) (n : ) :
real.cos ((n) * 2 * π - x) =
theorem real.cos_nat_mul_two_pi_add_pi (n : ) :
real.cos ((n) * 2 * π + π) = -1
theorem real.cos_int_mul_two_pi_add_pi (n : ) :
real.cos ((n) * 2 * π + π) = -1
theorem real.cos_nat_mul_two_pi_sub_pi (n : ) :
real.cos ((n) * 2 * π - π) = -1
theorem real.cos_int_mul_two_pi_sub_pi (n : ) :
real.cos ((n) * 2 * π - π) = -1
theorem real.sin_pos_of_pos_of_lt_pi {x : } (h0x : 0 < x) (hxp : x < π) :
0 <
theorem real.sin_pos_of_mem_Ioo {x : } (hx : x π) :
0 <
theorem real.sin_nonneg_of_mem_Icc {x : } (hx : x π) :
0
theorem real.sin_nonneg_of_nonneg_of_le_pi {x : } (h0x : 0 x) (hxp : x π) :
0
theorem real.sin_neg_of_neg_of_neg_pi_lt {x : } (hx0 : x < 0) (hpx : -π < x) :
< 0
theorem real.sin_nonpos_of_nonnpos_of_neg_pi_le {x : } (hx0 : x 0) (hpx : -π x) :
0
@[simp]
theorem real.sin_pi_div_two  :
real.sin (π / 2) = 1
theorem real.sin_add_pi_div_two (x : ) :
real.sin (x + π / 2) =
theorem real.sin_sub_pi_div_two (x : ) :
real.sin (x - π / 2) =
theorem real.sin_pi_div_two_sub (x : ) :
real.sin (π / 2 - x) =
theorem real.cos_add_pi_div_two (x : ) :
real.cos (x + π / 2) =
theorem real.cos_sub_pi_div_two (x : ) :
real.cos (x - π / 2) =
theorem real.cos_pi_div_two_sub (x : ) :
real.cos (π / 2 - x) =
theorem real.cos_pos_of_mem_Ioo {x : } (hx : x set.Ioo (-(π / 2)) (π / 2)) :
0 <
theorem real.cos_nonneg_of_mem_Icc {x : } (hx : x set.Icc (-(π / 2)) (π / 2)) :
0
theorem real.cos_nonneg_of_neg_pi_div_two_le_of_le {x : } (hl : -(π / 2) x) (hu : x π / 2) :
0
theorem real.cos_neg_of_pi_div_two_lt_of_lt {x : } (hx₁ : π / 2 < x) (hx₂ : x < π + π / 2) :
< 0
theorem real.cos_nonpos_of_pi_div_two_le_of_le {x : } (hx₁ : π / 2 x) (hx₂ : x π + π / 2) :
0
theorem real.sin_eq_sqrt_one_sub_cos_sq {x : } (hl : 0 x) (hu : x π) :
= real.sqrt (1 - ^ 2)
theorem real.cos_eq_sqrt_one_sub_sin_sq {x : } (hl : -(π / 2) x) (hu : x π / 2) :
= real.sqrt (1 - ^ 2)
theorem real.sin_eq_zero_iff_of_lt_of_lt {x : } (hx₁ : -π < x) (hx₂ : x < π) :
= 0 x = 0
theorem real.sin_eq_zero_iff {x : } :
= 0 ∃ (n : ), (n) * π = x
theorem real.sin_ne_zero_iff {x : } :
0 ∀ (n : ), (n) * π x
theorem real.sin_eq_zero_iff_cos_eq {x : } :
= 0 = 1 = -1
theorem real.cos_eq_one_iff (x : ) :
= 1 ∃ (n : ), (n) * 2 * π = x
theorem real.cos_eq_one_iff_of_lt_of_lt {x : } (hx₁ : -2 * π < x) (hx₂ : x < 2 * π) :
= 1 x = 0
theorem real.cos_lt_cos_of_nonneg_of_le_pi_div_two {x y : } (hx₁ : 0 x) (hy₂ : y π / 2) (hxy : x < y) :
theorem real.cos_lt_cos_of_nonneg_of_le_pi {x y : } (hx₁ : 0 x) (hy₂ : y π) (hxy : x < y) :
theorem real.cos_le_cos_of_nonneg_of_le_pi {x y : } (hx₁ : 0 x) (hy₂ : y π) (hxy : x y) :
theorem real.sin_lt_sin_of_lt_of_le_pi_div_two {x y : } (hx₁ : -(π / 2) x) (hy₂ : y π / 2) (hxy : x < y) :
theorem real.strict_mono_incr_on_sin  :
(set.Icc (-(π / 2)) (π / 2))
theorem real.sin_le_sin_of_le_of_le_pi_div_two {x y : } (hx₁ : -(π / 2) x) (hy₂ : y π / 2) (hxy : x y) :
theorem real.inj_on_sin  :
(set.Icc (-(π / 2)) (π / 2))
theorem real.inj_on_cos  :
theorem real.surj_on_sin  :
(set.Icc (-(π / 2)) (π / 2)) (set.Icc (-1) 1)
theorem real.surj_on_cos  :
(set.Icc (-1) 1)
theorem real.sin_mem_Icc (x : ) :
set.Icc (-1) 1
theorem real.cos_mem_Icc (x : ) :
set.Icc (-1) 1
theorem real.maps_to_sin (s : set ) :
(set.Icc (-1) 1)
theorem real.maps_to_cos (s : set ) :
(set.Icc (-1) 1)
theorem real.bij_on_sin  :
(set.Icc (-(π / 2)) (π / 2)) (set.Icc (-1) 1)
theorem real.bij_on_cos  :
(set.Icc (-1) 1)
@[simp]
theorem real.range_cos  :
= set.Icc (-1) 1
@[simp]
theorem real.range_sin  :
= set.Icc (-1) 1
theorem real.sin_lt {x : } (h : 0 < x) :
< x
theorem real.sin_gt_sub_cube {x : } (h : 0 < x) (h' : x 1) :
x - x ^ 3 / 4 <
@[simp]
def real.sqrt_two_add_series (x : ) :

the series `sqrt_two_add_series x n` is `sqrt(2 + sqrt(2 + ... ))` with `n` square roots, starting with `x`. We define it here because `cos (pi / 2 ^ (n+1)) = sqrt_two_add_series 0 n / 2`

Equations
theorem real.sqrt_two_add_series_nonneg {x : } (h : 0 x) (n : ) :
theorem real.sqrt_two_add_series_monotone_left {x y : } (h : x y) (n : ) :
@[simp]
theorem real.cos_pi_over_two_pow (n : ) :
real.cos (π / 2 ^ (n + 1)) =
theorem real.sin_sq_pi_over_two_pow (n : ) :
real.sin (π / 2 ^ (n + 1)) ^ 2 = 1 - / 2) ^ 2
theorem real.sin_sq_pi_over_two_pow_succ (n : ) :
real.sin (π / 2 ^ (n + 2)) ^ 2 = 1 / 2 -
@[simp]
theorem real.sin_pi_over_two_pow_succ (n : ) :
real.sin (π / 2 ^ (n + 2)) = real.sqrt (2 - / 2
@[simp]
theorem real.cos_pi_div_four  :
real.cos (π / 4) = / 2
@[simp]
theorem real.sin_pi_div_four  :
real.sin (π / 4) = / 2
@[simp]
theorem real.cos_pi_div_eight  :
@[simp]
theorem real.sin_pi_div_eight  :
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem real.cos_pi_div_three  :
real.cos (π / 3) = 1 / 2

The cosine of `π / 3` is `1 / 2`.

theorem real.sq_cos_pi_div_six  :
real.cos (π / 6) ^ 2 = 3 / 4

The square of the cosine of `π / 6` is `3 / 4` (this is sometimes more convenient than the result for cosine itself).

@[simp]
theorem real.cos_pi_div_six  :
real.cos (π / 6) = / 2

The cosine of `π / 6` is `√3 / 2`.

@[simp]
theorem real.sin_pi_div_six  :
real.sin (π / 6) = 1 / 2

The sine of `π / 6` is `1 / 2`.

theorem real.sq_sin_pi_div_three  :
real.sin (π / 3) ^ 2 = 3 / 4

The square of the sine of `π / 3` is `3 / 4` (this is sometimes more convenient than the result for cosine itself).

@[simp]
theorem real.sin_pi_div_three  :
real.sin (π / 3) = / 2

The sine of `π / 3` is `√3 / 2`.

def real.angle  :
Type

The type of angles

Equations
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
@[simp]
theorem real.angle.coe_zero  :
0 = 0
@[simp]
theorem real.angle.coe_add (x y : ) :
(x + y) = x + y
@[simp]
theorem real.angle.coe_neg (x : ) :
@[simp]
theorem real.angle.coe_sub (x y : ) :
(x - y) = x - y
@[simp]
theorem real.angle.coe_nat_mul_eq_nsmul (x : ) (n : ) :
(n) * x = n x
@[simp]
theorem real.angle.coe_int_mul_eq_gsmul (x : ) (n : ) :
(n) * x = n x
@[simp]
theorem real.angle.coe_two_pi  :
2 * π = 0
theorem real.angle.angle_eq_iff_two_pi_dvd_sub {ψ θ : } :
θ = ψ ∃ (k : ), θ - ψ = (2 * π) * k
theorem real.angle.cos_sin_inj {θ ψ : } (Hcos : = ) (Hsin : = ) :
θ = ψ
def real.sin_order_iso  :
(set.Icc (-(π / 2)) (π / 2)) ≃o (set.Icc (-1) 1)

`real.sin` as an `order_iso` between `[-(π / 2), π / 2]` and `[-1, 1]`.

Equations
@[simp]
theorem real.coe_sin_order_iso_apply (x : (set.Icc (-(π / 2)) (π / 2))) :
theorem real.sin_order_iso_apply (x : (set.Icc (-(π / 2)) (π / 2))) :
= , _⟩
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
theorem real.arcsin_mem_Icc (x : ) :
set.Icc (-(π / 2)) (π / 2)
@[simp]
theorem real.range_arcsin  :
= set.Icc (-(π / 2)) (π / 2)
theorem real.sin_arcsin' {x : } (hx : x set.Icc (-1) 1) :
= x
theorem real.sin_arcsin {x : } (hx₁ : -1 x) (hx₂ : x 1) :
= x
theorem real.arcsin_sin' {x : } (hx : x set.Icc (-(π / 2)) (π / 2)) :
= x
theorem real.arcsin_sin {x : } (hx₁ : -(π / 2) x) (hx₂ : x π / 2) :
= x
theorem real.inj_on_arcsin  :
(set.Icc (-1) 1)
theorem real.arcsin_inj {x y : } (hx₁ : -1 x) (hx₂ : x 1) (hy₁ : -1 y) (hy₂ : y 1) :
x = y
theorem real.arcsin_eq_of_sin_eq {x y : } (h₁ : = y) (h₂ : x set.Icc (-(π / 2)) (π / 2)) :
= x
@[simp]
theorem real.arcsin_zero  :
= 0
@[simp]
theorem real.arcsin_one  :
= π / 2
theorem real.arcsin_of_one_le {x : } (hx : 1 x) :
= π / 2
theorem real.arcsin_neg_one  :
real.arcsin (-1) = -(π / 2)
theorem real.arcsin_of_le_neg_one {x : } (hx : x -1) :
= -(π / 2)
@[simp]
theorem real.arcsin_neg (x : ) :
theorem real.arcsin_le_iff_le_sin {x y : } (hx : x set.Icc (-1) 1) (hy : y set.Icc (-(π / 2)) (π / 2)) :
y x
theorem real.arcsin_le_iff_le_sin' {x y : } (hy : y set.Ico (-(π / 2)) (π / 2)) :
y x
theorem real.le_arcsin_iff_sin_le {x y : } (hx : x set.Icc (-(π / 2)) (π / 2)) (hy : y set.Icc (-1) 1) :
x y
theorem real.le_arcsin_iff_sin_le' {x y : } (hx : x set.Ioc (-(π / 2)) (π / 2)) :
x y
theorem real.arcsin_lt_iff_lt_sin {x y : } (hx : x set.Icc (-1) 1) (hy : y set.Icc (-(π / 2)) (π / 2)) :
< y x <
theorem real.arcsin_lt_iff_lt_sin' {x y : } (hy : y set.Ioc (-(π / 2)) (π / 2)) :
< y x <
theorem real.lt_arcsin_iff_sin_lt {x y : } (hx : x set.Icc (-(π / 2)) (π / 2)) (hy : y set.Icc (-1) 1) :
x < < y
theorem real.lt_arcsin_iff_sin_lt' {x y : } (hx : x set.Ico (-(π / 2)) (π / 2)) :
x < < y
theorem real.arcsin_eq_iff_eq_sin {x y : } (hy : y set.Ioo (-(π / 2)) (π / 2)) :
= y x =
@[simp]
theorem real.arcsin_nonneg {x : } :
0 0 x
@[simp]
theorem real.arcsin_nonpos {x : } :
0 x 0
@[simp]
theorem real.arcsin_eq_zero_iff {x : } :
= 0 x = 0
@[simp]
theorem real.zero_eq_arcsin_iff {x : } :
0 = x = 0
@[simp]
theorem real.arcsin_pos {x : } :
0 < 0 < x
@[simp]
theorem real.arcsin_lt_zero {x : } :
< 0 x < 0
@[simp]
theorem real.arcsin_lt_pi_div_two {x : } :
< π / 2 x < 1
@[simp]
theorem real.neg_pi_div_two_lt_arcsin {x : } :
-(π / 2) < -1 < x
@[simp]
theorem real.arcsin_eq_pi_div_two {x : } :
= π / 2 1 x
@[simp]
theorem real.pi_div_two_eq_arcsin {x : } :
π / 2 = 1 x
@[simp]
theorem real.pi_div_two_le_arcsin {x : } :
π / 2 1 x
@[simp]
theorem real.arcsin_eq_neg_pi_div_two {x : } :
= -(π / 2) x -1
@[simp]
theorem real.neg_pi_div_two_eq_arcsin {x : } :
-(π / 2) = x -1
@[simp]
theorem real.arcsin_le_neg_pi_div_two {x : } :
-(π / 2) x -1
theorem real.maps_to_sin_Ioo  :
(set.Ioo (-(π / 2)) (π / 2)) (set.Ioo (-1) 1)
@[simp]

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

Equations
theorem real.cos_arcsin_nonneg (x : ) :
0
theorem real.cos_arcsin {x : } (hx₁ : -1 x) (hx₂ : x 1) :
= real.sqrt (1 - x ^ 2)
theorem real.deriv_arcsin_aux {x : } (h₁ : x -1) (h₂ : x 1) :
(1 / real.sqrt (1 - x ^ 2)) x
theorem real.has_strict_deriv_at_arcsin {x : } (h₁ : x -1) (h₂ : x 1) :
(1 / real.sqrt (1 - x ^ 2)) x
theorem real.has_deriv_at_arcsin {x : } (h₁ : x -1) (h₂ : x 1) :
(1 / real.sqrt (1 - x ^ 2)) x
theorem real.times_cont_diff_at_arcsin {x : } (h₁ : x -1) (h₂ : x 1) {n : with_top } :
theorem real.has_deriv_within_at_arcsin_Ici {x : } (h : x -1) :
(1 / real.sqrt (1 - x ^ 2)) (set.Ici x) x
theorem real.has_deriv_within_at_arcsin_Iic {x : } (h : x 1) :
(1 / real.sqrt (1 - x ^ 2)) (set.Iic x) x
theorem real.differentiable_at_arcsin {x : } :
x -1 x 1
@[simp]
theorem real.deriv_arcsin  :
= λ (x : ), 1 / real.sqrt (1 - x ^ 2)
theorem real.times_cont_diff_at_arcsin_iff {x : } {n : with_top } :
n = 0 x -1 x 1
def real.arccos (x : ) :

Inverse of the `cos` function, returns values in the range `0 ≤ arccos x` and `arccos x ≤ π`. If the argument is not between `-1` and `1` it defaults to `π / 2`

Equations
theorem real.arccos_le_pi (x : ) :
theorem real.arccos_nonneg (x : ) :
0
theorem real.cos_arccos {x : } (hx₁ : -1 x) (hx₂ : x 1) :
= x