ofReal_arctan — Mathlib

English

For any real x, the complex arctan of x equals the real arctan lifted to the complex plane.

Русский

Для любого действительного x комплексный arctan x равен вещественному arctan x, помещённому в комплексное поле.

LaTeX

$$$\\forall x \\in \\mathbb{R},\\; (\\operatorname{Real.arctan} x : \\mathbb{C}) = \\operatorname{arctan} x.$$$

Lean4

@[simp, norm_cast]
theorem ofReal_arctan (x : ℝ) : (Real.arctan x : ℂ) = arctan x :=
  by
  conv_rhs => rw [← Real.tan_arctan x]
  rw [ofReal_tan, arctan_tan]
  all_goals norm_cast
  · rw [← ne_eq]; exact (Real.arctan_lt_pi_div_two _).ne
  · exact Real.neg_pi_div_two_lt_arctan _
  · exact (Real.arctan_lt_pi_div_two _).le

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