hasDerivAt_tan_of_mem_Ioo — Mathlib

English

If x lies in the open interval (-π/2, π/2), then has derivative of tan is 1/cos^2 x.

Русский

Если x лежит в окне (-π/2, π/2), то для tan имеют производную 1/cos^2 x.

LaTeX

$$$ \text{hasDerivAt_tan_of_mem_Ioo }\{x : \mathbb{R}\} \Rightarrow \text{HasDerivAt } \tan (1/\cos^2 x) x. $$$

Lean4

theorem hasDerivAt_tan_of_mem_Ioo {x : ℝ} (h : x ∈ Ioo (-(π / 2) : ℝ) (π / 2)) : HasDerivAt tan (1 / cos x ^ 2) x :=
  hasDerivAt_tan (cos_pos_of_mem_Ioo h).ne'

Похожие утверждения