differentiableAt_tan — Mathlib

English

For every x in the complex plane, tan is differentiable at x if and only if cos x ≠ 0.

Русский

Для каждого x из комплексной плоскости тангенс дифференцируем в точке x тогда и только тогда, когда cos x ≠ 0.

LaTeX

$$$$\forall x \in \mathbb{C}, \; \mathrm{DifferentiableAt}(\mathbb{C}, \tan x) \iff \cos x \neq 0.$$$$

Lean4

@[simp]
theorem differentiableAt_tan {x : ℂ} : DifferentiableAt ℂ tan x ↔ cos x ≠ 0 :=
  ⟨fun h => continuousAt_tan.1 h.continuousAt, fun h => (hasDerivAt_tan h).differentiableAt⟩

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