# mathlibdocumentation

analysis.special_functions.trigonometric.deriv

# Differentiability of trigonometric functions #

## Main statements #

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

## Tags #

sin, cos, tan, angle

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 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 cont_diff_at.ccos {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {n : with_top } (hf : f x) :
(λ (x : E), complex.cos (f x)) x
theorem cont_diff_on.ccos {E : Type u_1} [normed_group E] [ E] {f : E → } {s : set E} {n : with_top } (hf : f s) :
(λ (x : E), complex.cos (f x)) s
theorem cont_diff_within_at.ccos {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : s 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 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 cont_diff_at.csin {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {n : with_top } (hf : f x) :
(λ (x : E), complex.sin (f x)) x
theorem cont_diff_on.csin {E : Type u_1} [normed_group E] [ E] {f : E → } {s : set E} {n : with_top } (hf : f s) :
(λ (x : E), complex.sin (f x)) s
theorem cont_diff_within_at.csin {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : s 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 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 cont_diff_at.ccosh {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {n : with_top } (hf : f x) :
(λ (x : E), complex.cosh (f x)) x
theorem cont_diff_on.ccosh {E : Type u_1} [normed_group E] [ E] {f : E → } {s : set E} {n : with_top } (hf : f s) :
(λ (x : E), complex.cosh (f x)) s
theorem cont_diff_within_at.ccosh {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : s 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 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 cont_diff_at.csinh {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {n : with_top } (hf : f x) :
(λ (x : E), complex.sinh (f x)) x
theorem cont_diff_on.csinh {E : Type u_1} [normed_group E] [ E] {f : E → } {s : set E} {n : with_top } (hf : f s) :
(λ (x : E), complex.sinh (f x)) s
theorem cont_diff_within_at.csinh {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : s 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.

`sinh` is injective, `∀ a b, sinh a = sinh b → a = b`.

@[simp]
theorem real.sinh_inj {x y : } :
x = y
@[simp]
theorem real.sinh_le_sinh {x y : } :
x y
@[simp]
theorem real.sinh_lt_sinh {x y : } :
x < y
@[simp]
theorem real.sinh_pos_iff {x : } :
0 < 0 < x
@[simp]
theorem real.sinh_nonpos_iff {x : } :
0 x 0
@[simp]
theorem real.sinh_neg_iff {x : } :
< 0 x < 0
@[simp]
theorem real.sinh_nonneg_iff {x : } :
0 0 x
@[simp]
theorem real.cosh_le_cosh {x y : } :
@[simp]
theorem real.cosh_lt_cosh {x y : } :
|x| < |y|
@[simp]
theorem real.one_le_cosh (x : ) :
1
@[simp]
theorem real.one_lt_cosh {x : } :
1 < x 0
@[simp]
theorem real.self_le_sinh_iff {x : } :
x 0 x
@[simp]
theorem real.sinh_le_self_iff {x : } :
x x 0
@[simp]
theorem real.self_lt_sinh_iff {x : } :
x < 0 < x
@[simp]
theorem real.sinh_lt_self_iff {x : } :
< x x < 0

### 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 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 cont_diff_at.cos {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {n : with_top } (hf : f x) :
(λ (x : E), real.cos (f x)) x
theorem cont_diff_on.cos {E : Type u_1} [normed_group E] [ E] {f : E → } {s : set E} {n : with_top } (hf : f s) :
(λ (x : E), real.cos (f x)) s
theorem cont_diff_within_at.cos {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : s 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 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 cont_diff_at.sin {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {n : with_top } (hf : f x) :
(λ (x : E), real.sin (f x)) x
theorem cont_diff_on.sin {E : Type u_1} [normed_group E] [ E] {f : E → } {s : set E} {n : with_top } (hf : f s) :
(λ (x : E), real.sin (f x)) s
theorem cont_diff_within_at.sin {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : s 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 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 cont_diff_at.cosh {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {n : with_top } (hf : f x) :
(λ (x : E), real.cosh (f x)) x
theorem cont_diff_on.cosh {E : Type u_1} [normed_group E] [ E] {f : E → } {s : set E} {n : with_top } (hf : f s) :
(λ (x : E), real.cosh (f x)) s
theorem cont_diff_within_at.cosh {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : s 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 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 cont_diff_at.sinh {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {n : with_top } (hf : f x) :
(λ (x : E), real.sinh (f x)) x
theorem cont_diff_on.sinh {E : Type u_1} [normed_group E] [ E] {f : E → } {s : set E} {n : with_top } (hf : f s) :
(λ (x : E), real.sinh (f x)) s
theorem cont_diff_within_at.sinh {E : Type u_1} [normed_group E] [ E] {f : E → } {x : E} {s : set E} {n : with_top } (hf : s x) :
(λ (x : E), real.sinh (f x)) s x