tan_sub' — Mathlib

English

If x and y avoid odd multiples of π/2, then tan(x−y) equals (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_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)

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