contDiffAt_tan — Mathlib

English

For every x, and every natural order of differentiability, tan is ContDiff at x iff cos x ≠ 0.

Русский

Для каждого x и любого уровня гладкости, tan принадлежит к классу ContDiff в точке x тогда, когда cos x ≠ 0.

LaTeX

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

Lean4

@[simp]
theorem contDiffAt_tan {x : ℂ} {n : WithTop ℕ∞} : ContDiffAt ℂ n tan x ↔ cos x ≠ 0 :=
  ⟨fun h => continuousAt_tan.1 h.continuousAt, contDiff_sin.contDiffAt.div contDiff_cos.contDiffAt⟩

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