tan_add' — Mathlib

English

If x and y avoid odd multiples of π/2, then tan(x+y) = (tan x + tan y) / (1 − tan x tan y).

Русский

Если x и y не являются нечетными кратными π/2, то tan(x+y) = (tan x + tan y) / (1 − tan x tan y).

LaTeX

$$$ ( \forall k \in \mathbb{Z}, x \neq (2k+1) \frac{\pi}{2} ) \land ( \forall l \in \mathbb{Z}, y \neq (2l+1) \frac{\pi}{2} ) \\Rightarrow \ tan(x+y) = \frac{\tan x + \tan y}{1 - \tan x \tan y} $$$

Lean4

theorem tan_add' (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_add (Or.inl h)

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