The arctan
function. #
Inequalities, derivatives,
and Real.tan
as a LocalHomeomorph
between (-(π / 2), π / 2)
and the whole line.
theorem
Real.arcsin_eq_arctan
{x : ℝ}
(h : x ∈ Set.Ioo (-1) 1)
:
Real.arcsin x = Real.arctan (x / Real.sqrt (↑1 - x ^ 2))
theorem
Real.arctan_eq_arccos
{x : ℝ}
(h : 0 ≤ x)
:
Real.arctan x = Real.arccos (Real.sqrt (↑1 + x ^ 2))⁻¹
theorem
Real.arccos_eq_arctan
{x : ℝ}
(h : 0 < x)
:
Real.arccos x = Real.arctan (Real.sqrt (↑1 - x ^ 2) / x)
Real.tan
as a LocalHomeomorph
between (-(π / 2), π / 2)
and the whole line.
Instances For
@[simp]