mathlib documentation

analysis.special_functions.trigonometric.basic

Trigonometric functions #

Main definitions #

This file contains the definition of π.

See also analysis.special_functions.trigonometric.inverse and analysis.special_functions.trigonometric.arctan for the inverse trigonometric functions.

See also analysis.special_functions.complex.arg and analysis.special_functions.complex.log for the complex argument function and the complex logarithm.

Main statements #

Many basic inequalities on the real trigonometric functions are established.

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

Several facts about the real trigonometric functions have the proofs deferred to analysis.special_functions.trigonometric.complex, as they are most easily proved by appealing to the corresponding fact for complex trigonometric functions.

See also analysis.special_functions.trigonometric.chebyshev for the multiple angle formulas in terms of Chebyshev polynomials.

Tags #

sin, cos, tan, angle

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

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

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

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

@[simp]

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

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

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

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

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

complex.cos #

theorem has_strict_deriv_at.ccos {f : } {f' x : } (hf : has_strict_deriv_at f f' 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 : has_deriv_at f 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 : has_deriv_within_at f f' 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 : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
deriv_within (λ (x : ), complex.cos (f x)) s x = (-complex.sin (f x)) * deriv_within f s x
@[simp]
theorem deriv_ccos {f : } {x : } (hc : differentiable_at f x) :
deriv (λ (x : ), complex.cos (f x)) x = (-complex.sin (f x)) * deriv f x

complex.sin #

theorem has_strict_deriv_at.csin {f : } {f' x : } (hf : has_strict_deriv_at f f' 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 : has_deriv_at f 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 : has_deriv_within_at f f' 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 : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
deriv_within (λ (x : ), complex.sin (f x)) s x = (complex.cos (f x)) * deriv_within f s x
@[simp]
theorem deriv_csin {f : } {x : } (hc : differentiable_at f x) :
deriv (λ (x : ), complex.sin (f x)) x = (complex.cos (f x)) * deriv f x

complex.cosh #

theorem has_strict_deriv_at.ccosh {f : } {f' x : } (hf : has_strict_deriv_at f f' 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 : has_deriv_at f 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 : has_deriv_within_at f f' 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 : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
deriv_within (λ (x : ), complex.cosh (f x)) s x = (complex.sinh (f x)) * deriv_within f s x
@[simp]
theorem deriv_ccosh {f : } {x : } (hc : differentiable_at f x) :
deriv (λ (x : ), complex.cosh (f x)) x = (complex.sinh (f x)) * deriv f x

complex.sinh #

theorem has_strict_deriv_at.csinh {f : } {f' x : } (hf : has_strict_deriv_at f f' 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 : has_deriv_at f 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 : has_deriv_within_at f f' 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 : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
deriv_within (λ (x : ), complex.sinh (f x)) s x = (complex.cosh (f x)) * deriv_within f s x
@[simp]
theorem deriv_csinh {f : } {x : } (hc : differentiable_at f x) :
deriv (λ (x : ), complex.sinh (f x)) x = (complex.cosh (f x)) * deriv f 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] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_strict_fderiv_at f f' 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] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_fderiv_at f 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] [normed_space E] {f : E → } {f' : E →L[] } {x : E} {s : set E} (hf : has_fderiv_within_at f f' 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] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) :
differentiable_within_at (λ (x : E), complex.cos (f x)) s x
@[simp]
theorem differentiable_at.ccos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
differentiable_at (λ (x : E), complex.cos (f x)) x
theorem differentiable_on.ccos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} (hc : differentiable_on f s) :
differentiable_on (λ (x : E), complex.cos (f x)) s
@[simp]
theorem differentiable.ccos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } (hc : differentiable f) :
differentiable (λ (x : E), complex.cos (f x))
theorem fderiv_within_ccos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
fderiv_within (λ (x : E), complex.cos (f x)) s x = -complex.sin (f x) fderiv_within f s x
@[simp]
theorem fderiv_ccos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
fderiv (λ (x : E), complex.cos (f x)) x = -complex.sin (f x) fderiv f x
theorem times_cont_diff.ccos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {n : with_top } (h : times_cont_diff n f) :
times_cont_diff n (λ (x : E), complex.cos (f x))
theorem times_cont_diff_at.ccos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {n : with_top } (hf : times_cont_diff_at n f x) :
times_cont_diff_at n (λ (x : E), complex.cos (f x)) x
theorem times_cont_diff_on.ccos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} {n : with_top } (hf : times_cont_diff_on n f s) :
times_cont_diff_on n (λ (x : E), complex.cos (f x)) s
theorem times_cont_diff_within_at.ccos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : times_cont_diff_within_at n f s x) :
times_cont_diff_within_at n (λ (x : E), complex.cos (f x)) s x

complex.sin #

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

complex.cosh #

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

complex.sinh #

theorem has_strict_fderiv_at.csinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_strict_fderiv_at f f' 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] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_fderiv_at f 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] [normed_space E] {f : E → } {f' : E →L[] } {x : E} {s : set E} (hf : has_fderiv_within_at f f' 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] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) :
differentiable_within_at (λ (x : E), complex.sinh (f x)) s x
@[simp]
theorem differentiable_at.csinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
differentiable_at (λ (x : E), complex.sinh (f x)) x
theorem differentiable_on.csinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} (hc : differentiable_on f s) :
differentiable_on (λ (x : E), complex.sinh (f x)) s
@[simp]
theorem differentiable.csinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } (hc : differentiable f) :
differentiable (λ (x : E), complex.sinh (f x))
theorem fderiv_within_csinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
fderiv_within (λ (x : E), complex.sinh (f x)) s x = complex.cosh (f x) fderiv_within f s x
@[simp]
theorem fderiv_csinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
fderiv (λ (x : E), complex.sinh (f x)) x = complex.cosh (f x) fderiv f x
theorem times_cont_diff.csinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {n : with_top } (h : times_cont_diff n f) :
times_cont_diff n (λ (x : E), complex.sinh (f x))
theorem times_cont_diff_at.csinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {n : with_top } (hf : times_cont_diff_at n f x) :
times_cont_diff_at n (λ (x : E), complex.sinh (f x)) x
theorem times_cont_diff_on.csinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} {n : with_top } (hf : times_cont_diff_on n f s) :
times_cont_diff_on n (λ (x : E), complex.sinh (f x)) s
theorem times_cont_diff_within_at.csinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : times_cont_diff_within_at n f s x) :
times_cont_diff_within_at n (λ (x : E), complex.sinh (f x)) s x
@[simp]
theorem real.deriv_cos'  :

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 : has_strict_deriv_at f f' 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 : has_deriv_at f 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 : has_deriv_within_at f f' 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 : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
deriv_within (λ (x : ), real.cos (f x)) s x = (-real.sin (f x)) * deriv_within f s x
@[simp]
theorem deriv_cos {f : } {x : } (hc : differentiable_at f x) :
deriv (λ (x : ), real.cos (f x)) x = (-real.sin (f x)) * deriv f x

real.sin #

theorem has_strict_deriv_at.sin {f : } {f' x : } (hf : has_strict_deriv_at f f' 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 : has_deriv_at f 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 : has_deriv_within_at f f' 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 : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
deriv_within (λ (x : ), real.sin (f x)) s x = (real.cos (f x)) * deriv_within f s x
@[simp]
theorem deriv_sin {f : } {x : } (hc : differentiable_at f x) :
deriv (λ (x : ), real.sin (f x)) x = (real.cos (f x)) * deriv f x

real.cosh #

theorem has_strict_deriv_at.cosh {f : } {f' x : } (hf : has_strict_deriv_at f f' 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 : has_deriv_at f 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 : has_deriv_within_at f f' 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 : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
deriv_within (λ (x : ), real.cosh (f x)) s x = (real.sinh (f x)) * deriv_within f s x
@[simp]
theorem deriv_cosh {f : } {x : } (hc : differentiable_at f x) :
deriv (λ (x : ), real.cosh (f x)) x = (real.sinh (f x)) * deriv f x

real.sinh #

theorem has_strict_deriv_at.sinh {f : } {f' x : } (hf : has_strict_deriv_at f f' 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 : has_deriv_at f 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 : has_deriv_within_at f f' 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 : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
deriv_within (λ (x : ), real.sinh (f x)) s x = (real.cosh (f x)) * deriv_within f s x
@[simp]
theorem deriv_sinh {f : } {x : } (hc : differentiable_at f x) :
deriv (λ (x : ), real.sinh (f x)) x = (real.cosh (f x)) * deriv f 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] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_strict_fderiv_at f f' 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] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_fderiv_at f 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] [normed_space E] {f : E → } {f' : E →L[] } {x : E} {s : set E} (hf : has_fderiv_within_at f f' 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] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) :
differentiable_within_at (λ (x : E), real.cos (f x)) s x
@[simp]
theorem differentiable_at.cos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
differentiable_at (λ (x : E), real.cos (f x)) x
theorem differentiable_on.cos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} (hc : differentiable_on f s) :
differentiable_on (λ (x : E), real.cos (f x)) s
@[simp]
theorem differentiable.cos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } (hc : differentiable f) :
differentiable (λ (x : E), real.cos (f x))
theorem fderiv_within_cos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
fderiv_within (λ (x : E), real.cos (f x)) s x = -real.sin (f x) fderiv_within f s x
@[simp]
theorem fderiv_cos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
fderiv (λ (x : E), real.cos (f x)) x = -real.sin (f x) fderiv f x
theorem times_cont_diff.cos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {n : with_top } (h : times_cont_diff n f) :
times_cont_diff n (λ (x : E), real.cos (f x))
theorem times_cont_diff_at.cos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {n : with_top } (hf : times_cont_diff_at n f x) :
times_cont_diff_at n (λ (x : E), real.cos (f x)) x
theorem times_cont_diff_on.cos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} {n : with_top } (hf : times_cont_diff_on n f s) :
times_cont_diff_on n (λ (x : E), real.cos (f x)) s
theorem times_cont_diff_within_at.cos {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : times_cont_diff_within_at n f s x) :
times_cont_diff_within_at n (λ (x : E), real.cos (f x)) s x

real.sin #

theorem has_strict_fderiv_at.sin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_strict_fderiv_at f f' 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] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_fderiv_at f 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] [normed_space E] {f : E → } {f' : E →L[] } {x : E} {s : set E} (hf : has_fderiv_within_at f f' 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] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) :
differentiable_within_at (λ (x : E), real.sin (f x)) s x
@[simp]
theorem differentiable_at.sin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
differentiable_at (λ (x : E), real.sin (f x)) x
theorem differentiable_on.sin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} (hc : differentiable_on f s) :
differentiable_on (λ (x : E), real.sin (f x)) s
@[simp]
theorem differentiable.sin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } (hc : differentiable f) :
differentiable (λ (x : E), real.sin (f x))
theorem fderiv_within_sin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
fderiv_within (λ (x : E), real.sin (f x)) s x = real.cos (f x) fderiv_within f s x
@[simp]
theorem fderiv_sin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
fderiv (λ (x : E), real.sin (f x)) x = real.cos (f x) fderiv f x
theorem times_cont_diff.sin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {n : with_top } (h : times_cont_diff n f) :
times_cont_diff n (λ (x : E), real.sin (f x))
theorem times_cont_diff_at.sin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {n : with_top } (hf : times_cont_diff_at n f x) :
times_cont_diff_at n (λ (x : E), real.sin (f x)) x
theorem times_cont_diff_on.sin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} {n : with_top } (hf : times_cont_diff_on n f s) :
times_cont_diff_on n (λ (x : E), real.sin (f x)) s
theorem times_cont_diff_within_at.sin {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : times_cont_diff_within_at n f s x) :
times_cont_diff_within_at n (λ (x : E), real.sin (f x)) s x

real.cosh #

theorem has_strict_fderiv_at.cosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_strict_fderiv_at f f' 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] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_fderiv_at f 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] [normed_space E] {f : E → } {f' : E →L[] } {x : E} {s : set E} (hf : has_fderiv_within_at f f' 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] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) :
differentiable_within_at (λ (x : E), real.cosh (f x)) s x
@[simp]
theorem differentiable_at.cosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
differentiable_at (λ (x : E), real.cosh (f x)) x
theorem differentiable_on.cosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} (hc : differentiable_on f s) :
differentiable_on (λ (x : E), real.cosh (f x)) s
@[simp]
theorem differentiable.cosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } (hc : differentiable f) :
differentiable (λ (x : E), real.cosh (f x))
theorem fderiv_within_cosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
fderiv_within (λ (x : E), real.cosh (f x)) s x = real.sinh (f x) fderiv_within f s x
@[simp]
theorem fderiv_cosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
fderiv (λ (x : E), real.cosh (f x)) x = real.sinh (f x) fderiv f x
theorem times_cont_diff.cosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {n : with_top } (h : times_cont_diff n f) :
times_cont_diff n (λ (x : E), real.cosh (f x))
theorem times_cont_diff_at.cosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {n : with_top } (hf : times_cont_diff_at n f x) :
times_cont_diff_at n (λ (x : E), real.cosh (f x)) x
theorem times_cont_diff_on.cosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} {n : with_top } (hf : times_cont_diff_on n f s) :
times_cont_diff_on n (λ (x : E), real.cosh (f x)) s
theorem times_cont_diff_within_at.cosh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : times_cont_diff_within_at n f s x) :
times_cont_diff_within_at n (λ (x : E), real.cosh (f x)) s x

real.sinh #

theorem has_strict_fderiv_at.sinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_strict_fderiv_at f f' 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] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (hf : has_fderiv_at f 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] [normed_space E] {f : E → } {f' : E →L[] } {x : E} {s : set E} (hf : has_fderiv_within_at f f' 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] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) :
differentiable_within_at (λ (x : E), real.sinh (f x)) s x
@[simp]
theorem differentiable_at.sinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
differentiable_at (λ (x : E), real.sinh (f x)) x
theorem differentiable_on.sinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} (hc : differentiable_on f s) :
differentiable_on (λ (x : E), real.sinh (f x)) s
@[simp]
theorem differentiable.sinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } (hc : differentiable f) :
differentiable (λ (x : E), real.sinh (f x))
theorem fderiv_within_sinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
fderiv_within (λ (x : E), real.sinh (f x)) s x = real.cosh (f x) fderiv_within f s x
@[simp]
theorem fderiv_sinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} (hc : differentiable_at f x) :
fderiv (λ (x : E), real.sinh (f x)) x = real.cosh (f x) fderiv f x
theorem times_cont_diff.sinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {n : with_top } (h : times_cont_diff n f) :
times_cont_diff n (λ (x : E), real.sinh (f x))
theorem times_cont_diff_at.sinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {n : with_top } (hf : times_cont_diff_at n f x) :
times_cont_diff_at n (λ (x : E), real.sinh (f x)) x
theorem times_cont_diff_on.sinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {s : set E} {n : with_top } (hf : times_cont_diff_on n f s) :
times_cont_diff_on n (λ (x : E), real.sinh (f x)) s
theorem times_cont_diff_within_at.sinh {E : Type u_1} [normed_group E] [normed_space E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : times_cont_diff_within_at n f s x) :
times_cont_diff_within_at n (λ (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.bounds.

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]
@[simp]
theorem real.sin_pi  :
@[simp]
theorem real.cos_pi  :
@[simp]
theorem real.sin_two_pi  :
real.sin (2 * π) = 0
@[simp]
theorem real.cos_two_pi  :
real.cos (2 * π) = 1
@[simp]
theorem real.sin_add_pi (x : ) :
@[simp]
theorem real.sin_add_two_pi (x : ) :
@[simp]
theorem real.sin_sub_pi (x : ) :
@[simp]
theorem real.sin_sub_two_pi (x : ) :
@[simp]
theorem real.sin_pi_sub (x : ) :
@[simp]
theorem real.sin_two_pi_sub (x : ) :
@[simp]
theorem real.sin_nat_mul_pi (n : ) :
real.sin ((n) * π) = 0
@[simp]
theorem real.sin_int_mul_pi (n : ) :
real.sin ((n) * π) = 0
@[simp]
theorem real.sin_add_nat_mul_two_pi (x : ) (n : ) :
real.sin (x + (n) * 2 * π) = real.sin x
@[simp]
theorem real.sin_add_int_mul_two_pi (x : ) (n : ) :
real.sin (x + (n) * 2 * π) = real.sin x
@[simp]
theorem real.sin_sub_nat_mul_two_pi (x : ) (n : ) :
real.sin (x - (n) * 2 * π) = real.sin x
@[simp]
theorem real.sin_sub_int_mul_two_pi (x : ) (n : ) :
real.sin (x - (n) * 2 * π) = real.sin x
@[simp]
theorem real.sin_nat_mul_two_pi_sub (x : ) (n : ) :
real.sin ((n) * 2 * π - x) = -real.sin x
@[simp]
theorem real.sin_int_mul_two_pi_sub (x : ) (n : ) :
real.sin ((n) * 2 * π - x) = -real.sin x
@[simp]
theorem real.cos_add_pi (x : ) :
@[simp]
theorem real.cos_add_two_pi (x : ) :
@[simp]
theorem real.cos_sub_pi (x : ) :
@[simp]
theorem real.cos_sub_two_pi (x : ) :
@[simp]
theorem real.cos_pi_sub (x : ) :
@[simp]
theorem real.cos_two_pi_sub (x : ) :
@[simp]
theorem real.cos_nat_mul_two_pi (n : ) :
real.cos ((n) * 2 * π) = 1
@[simp]
theorem real.cos_int_mul_two_pi (n : ) :
real.cos ((n) * 2 * π) = 1
@[simp]
theorem real.cos_add_nat_mul_two_pi (x : ) (n : ) :
real.cos (x + (n) * 2 * π) = real.cos x
@[simp]
theorem real.cos_add_int_mul_two_pi (x : ) (n : ) :
real.cos (x + (n) * 2 * π) = real.cos x
@[simp]
theorem real.cos_sub_nat_mul_two_pi (x : ) (n : ) :
real.cos (x - (n) * 2 * π) = real.cos x
@[simp]
theorem real.cos_sub_int_mul_two_pi (x : ) (n : ) :
real.cos (x - (n) * 2 * π) = real.cos x
@[simp]
theorem real.cos_nat_mul_two_pi_sub (x : ) (n : ) :
real.cos ((n) * 2 * π - x) = real.cos x
@[simp]
theorem real.cos_int_mul_two_pi_sub (x : ) (n : ) :
real.cos ((n) * 2 * π - x) = real.cos x
@[simp]
theorem real.cos_nat_mul_two_pi_add_pi (n : ) :
real.cos ((n) * 2 * π + π) = -1
@[simp]
theorem real.cos_int_mul_two_pi_add_pi (n : ) :
real.cos ((n) * 2 * π + π) = -1
@[simp]
theorem real.cos_nat_mul_two_pi_sub_pi (n : ) :
real.cos ((n) * 2 * π - π) = -1
@[simp]
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 < π) :
theorem real.sin_pos_of_mem_Ioo {x : } (hx : x set.Ioo 0 π) :
theorem real.sin_nonneg_of_mem_Icc {x : } (hx : x set.Icc 0 π) :
theorem real.sin_nonneg_of_nonneg_of_le_pi {x : } (h0x : 0 x) (hxp : x π) :
theorem real.sin_neg_of_neg_of_neg_pi_lt {x : } (hx0 : x < 0) (hpx : -π < x) :
theorem real.sin_nonpos_of_nonnpos_of_neg_pi_le {x : } (hx0 : x 0) (hpx : -π x) :
@[simp]
theorem real.sin_pi_div_two  :
real.sin (π / 2) = 1
theorem real.cos_pos_of_mem_Ioo {x : } (hx : x set.Ioo (-(π / 2)) (π / 2)) :
theorem real.cos_nonneg_of_mem_Icc {x : } (hx : x set.Icc (-(π / 2)) (π / 2)) :
theorem real.cos_nonneg_of_neg_pi_div_two_le_of_le {x : } (hl : -(π / 2) x) (hu : x π / 2) :
theorem real.cos_neg_of_pi_div_two_lt_of_lt {x : } (hx₁ : π / 2 < x) (hx₂ : x < π + π / 2) :
theorem real.cos_nonpos_of_pi_div_two_le_of_le {x : } (hx₁ : π / 2 x) (hx₂ : x π + π / 2) :
theorem real.sin_eq_sqrt_one_sub_cos_sq {x : } (hl : 0 x) (hu : x π) :
theorem real.cos_eq_sqrt_one_sub_sin_sq {x : } (hl : -(π / 2) x) (hu : x π / 2) :
theorem real.sin_eq_zero_iff_of_lt_of_lt {x : } (hx₁ : -π < x) (hx₂ : x < π) :
real.sin x = 0 x = 0
theorem real.sin_eq_zero_iff {x : } :
real.sin x = 0 ∃ (n : ), (n) * π = x
theorem real.sin_ne_zero_iff {x : } :
real.sin x 0 ∀ (n : ), (n) * π x
theorem real.cos_eq_one_iff (x : ) :
real.cos x = 1 ∃ (n : ), (n) * 2 * π = x
theorem real.cos_eq_one_iff_of_lt_of_lt {x : } (hx₁ : -2 * π < x) (hx₂ : x < 2 * π) :
real.cos x = 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.sin_le_sin_of_le_of_le_pi_div_two {x y : } (hx₁ : -(π / 2) x) (hy₂ : y π / 2) (hxy : x y) :
theorem real.surj_on_sin  :
set.surj_on real.sin (set.Icc (-(π / 2)) (π / 2)) (set.Icc (-1) 1)
theorem real.sin_mem_Icc (x : ) :
theorem real.cos_mem_Icc (x : ) :
theorem real.maps_to_sin (s : set ) :
theorem real.maps_to_cos (s : set ) :
theorem real.bij_on_sin  :
set.bij_on real.sin (set.Icc (-(π / 2)) (π / 2)) (set.Icc (-1) 1)
@[simp]
@[simp]
theorem real.sin_lt {x : } (h : 0 < x) :
theorem real.sin_gt_sub_cube {x : } (h : 0 < x) (h' : x 1) :
x - x ^ 3 / 4 < real.sin x
@[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
@[simp]
theorem real.cos_pi_over_two_pow (n : ) :
theorem real.sin_sq_pi_over_two_pow (n : ) :
real.sin (π / 2 ^ (n + 1)) ^ 2 = 1 - (real.sqrt_two_add_series 0 n / 2) ^ 2
@[simp]
@[simp]
theorem real.cos_pi_div_four  :
@[simp]
theorem real.sin_pi_div_four  :
@[simp]
@[simp]
@[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  :

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]

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

def real.angle  :
Type

The type of angles

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 : real.cos θ = real.cos ψ) (Hsin : real.sin θ = real.sin ψ) :
θ = ψ
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.tan_pi_div_four  :
real.tan (π / 4) = 1
@[simp]
theorem real.tan_pi_div_two  :
real.tan (π / 2) = 0
theorem real.tan_pos_of_pos_of_lt_pi_div_two {x : } (h0x : 0 < x) (hxp : x < π / 2) :
theorem real.tan_nonneg_of_nonneg_of_le_pi_div_two {x : } (h0x : 0 x) (hxp : x π / 2) :
theorem real.tan_neg_of_neg_of_pi_div_two_lt {x : } (hx0 : x < 0) (hpx : -(π / 2) < x) :
theorem real.tan_nonpos_of_nonpos_of_neg_pi_div_two_le {x : } (hx0 : x 0) (hpx : -(π / 2) x) :
theorem real.tan_lt_tan_of_nonneg_of_lt_pi_div_two {x y : } (hx₁ : 0 x) (hy₂ : y < π / 2) (hxy : x < y) :
theorem real.tan_lt_tan_of_lt_of_lt_pi_div_two {x y : } (hx₁ : -(π / 2) < x) (hy₂ : y < π / 2) (hxy : x < y) :
theorem real.tan_inj_of_lt_of_lt_pi_div_two {x y : } (hx₁ : -(π / 2) < x) (hx₂ : x < π / 2) (hy₁ : -(π / 2) < y) (hy₂ : y < π / 2) (hxy : real.tan x = real.tan y) :
x = y
theorem real.tan_add_pi (x : ) :
theorem real.tan_sub_pi (x : ) :
theorem real.tan_pi_sub (x : ) :
theorem real.tan_nat_mul_pi (n : ) :
real.tan ((n) * π) = 0
theorem real.tan_int_mul_pi (n : ) :
real.tan ((n) * π) = 0
theorem real.tan_add_nat_mul_pi (x : ) (n : ) :
theorem real.tan_add_int_mul_pi (x : ) (n : ) :
theorem real.tan_sub_nat_mul_pi (x : ) (n : ) :
theorem real.tan_sub_int_mul_pi (x : ) (n : ) :
theorem real.tan_nat_mul_pi_sub (x : ) (n : ) :
theorem real.tan_int_mul_pi_sub (x : ) (n : ) :
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem complex.sin_two_pi  :
@[simp]
theorem complex.cos_two_pi  :
theorem