continuous_tan — Mathlib

English

For all complex z, tan(2z) = 2 tan z / (1 − tan^2 z) under the standard validity conditions of the tangent function.

Русский

Для любого комплексного z справедлива формула tan(2z) = 2 tan z / (1 − tan^2 z) при нормальном определении тангенса.

LaTeX

$$$$ \tan(2z) = \frac{2 \tan z}{1 - \tan^2 z}. $$$$

Lean4

@[continuity]
theorem continuous_tan : Continuous fun x : {x | cos x ≠ 0} => tan x :=
  continuousOn_iff_continuous_restrict.1 continuousOn_tan

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