English
Let x,y be complex numbers avoiding odd multiples of π/2, i.e., x ≠ (2k+1)π/2 and y ≠ (2ℓ+1)π/2 for all integers k,ℓ. Then tan(x − y) = (tan x − tan y) / (1 + tan x tan y).
Русский
Пусть x,y ∈ ℂ такие, что ни x, ни y не являются нечётными кратными π/2, то есть x ≠ (2k+1)π/2 и y ≠ (2ℓ+1)π/2 для всех целых k,ℓ. Тогда tan(x − y) = (tan x − tan y) / (1 + tan x tan y).
LaTeX
$$$$ \tan(x - y) = \frac{\tan x - \tan y}{1 + \tan x \tan y}, \quad \text{при условии } x \neq (2k+1)\frac{\pi}{2},\ y \neq (2\ell+1)\frac{\pi}{2} \text{ для всех } k,\ell \in \mathbb{Z}. $$$$
Lean4
theorem tan_sub' {x y : ℂ} (h : (∀ k : ℤ, x ≠ (2 * k + 1) * π / 2) ∧ ∀ l : ℤ, y ≠ (2 * l + 1) * π / 2) :
tan (x - y) = (tan x - tan y) / (1 + tan x * tan y) :=
tan_sub (Or.inl h)
