arctan_add — Mathlib

English

If xy < 1, then arctan x + arctan y = arctan((x+y)/(1-xy)).

Русский

Если xy < 1, то arctan x + arctan y = arctan((x+y)/(1-xy)).

LaTeX

$$$xy < 1 \\Rightarrow \\arctan x + \\arctan y = \\arctan\\left(\\\\frac{x+y}{1-xy}\\\\right).$$$

Lean4

theorem arctan_add (h : x * y < 1) : arctan x + arctan y = arctan ((x + y) / (1 - x * y)) :=
  by
  rw [← arctan_tan (x := _ + _)]
  · congr
    conv_rhs => rw [← tan_arctan x, ← tan_arctan y]
    exact tan_add' ⟨arctan_ne_mul_pi_div_two, arctan_ne_mul_pi_div_two⟩
  · rw [neg_lt, neg_add, ← arctan_neg, ← arctan_neg]
    rw [← neg_mul_neg] at h
    exact arctan_add_arctan_lt_pi_div_two h
  · exact arctan_add_arctan_lt_pi_div_two h

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