# mathlib3documentation

analysis.special_functions.trigonometric.arctan

# The arctan function. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Inequalities, derivatives, and real.tan as a local_homeomorph between (-(π / 2), π / 2) and the whole line.

theorem real.tan_add {x y : } (h : (( (k : ), x (2 * k + 1) * real.pi / 2) (l : ), y (2 * l + 1) * real.pi / 2) ( (k : ), x = (2 * k + 1) * real.pi / 2) (l : ), y = (2 * l + 1) * real.pi / 2) :
real.tan (x + y) = (real.tan x + real.tan y) / (1 - * real.tan y)
theorem real.tan_add' {x y : } (h : ( (k : ), x (2 * k + 1) * real.pi / 2) (l : ), y (2 * l + 1) * real.pi / 2) :
real.tan (x + y) = (real.tan x + real.tan y) / (1 - * real.tan y)
theorem real.tan_two_mul {x : } :
real.tan (2 * x) = 2 * / (1 - ^ 2)
theorem real.tan_ne_zero_iff {θ : } :
0 (k : ), θ / 2
theorem real.tan_eq_zero_iff {θ : } :
= 0 (k : ), θ = / 2
theorem real.continuous_on_tan  :
{x : | 0}
@[continuity]
theorem real.continuous_tan  :
continuous (λ (x : {x : | 0}),
noncomputable def real.tan_order_iso  :

real.tan as an order_iso between (-(π / 2), π / 2) and ℝ.

Equations
noncomputable def real.arctan (x : ) :

Inverse of the tan function, returns values in the range -π / 2 < arctan x and arctan x < π / 2

Equations
@[simp]
theorem real.tan_arctan (x : ) :
= x
theorem real.arctan_mem_Ioo (x : ) :
@[simp]
theorem real.range_arctan  :
theorem real.arctan_tan {x : } (hx₁ : -(real.pi / 2) < x) (hx₂ : x < ) :
= x
theorem real.cos_arctan_pos (x : ) :
0 <
theorem real.cos_sq_arctan (x : ) :
^ 2 = 1 / (1 + x ^ 2)
theorem real.sin_arctan (x : ) :
= x / (1 + x ^ 2)
theorem real.cos_arctan (x : ) :
= 1 / (1 + x ^ 2)
theorem real.arctan_eq_arcsin (x : ) :
= real.arcsin (x / (1 + x ^ 2))
theorem real.arcsin_eq_arctan {x : } (h : x set.Ioo (-1) 1) :
= real.arctan (x / (1 - x ^ 2))
@[simp]
theorem real.arctan_zero  :
= 0
theorem real.arctan_eq_of_tan_eq {x y : } (h : = y) (hx : x set.Ioo (-(real.pi / 2)) (real.pi / 2)) :
= x
@[simp]
theorem real.arctan_one  :
=
@[simp]
theorem real.arctan_neg (x : ) :
theorem real.arctan_eq_arccos {x : } (h : 0 x) :
= real.arccos ( (1 + x ^ 2))⁻¹
theorem real.arccos_eq_arctan {x : } (h : 0 < x) :
= real.arctan ( (1 - x ^ 2) / x)
@[continuity]
noncomputable def real.tan_local_homeomorph  :

real.tan as a local_homeomorph between (-(π / 2), π / 2) and the whole line.

Equations
@[simp]
@[simp]