differentiableAt_tan_of_mem_Ioo

Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv

URI: https://scilib.ai/kg/mathlib#Real.differentiableAt_tan_of_mem_Ioo

← MathLib Explorer

English

If x ∈ Ioo(-π/2, π/2), then tan is differentiable at x.

Русский

Если x ∈ Ioo(-π/2, π/2), то тангенс дифференцируем в x.

LaTeX

$$$ \text{differentiableAt_tan_of_mem_Ioo } \{x : \mathbb{R}\} \Rightarrow \text{DifferentiableAt } \tan x. $$$

Lean4

theorem differentiableAt_tan_of_mem_Ioo {x : ℝ} (h : x ∈ Ioo (-(π / 2) : ℝ) (π / 2)) : DifferentiableAt ℝ tan x :=
  (hasDerivAt_tan_of_mem_Ioo h).differentiableAt

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru