arctan_eq_arccos — Mathlib

English

Let x ≥ 0. Then arctan x equals arccos(1/√(1+x^2)).

Русский

Пусть x ≥ 0. Тогда arctan x равно arccos(1/√(1+x^2)).

LaTeX

$$$\\\\arctan x = \\\\arccos\\\\left(\\\\frac{1}{\\\\sqrt{1+x^2}}\\\\right), \\\\quad x \ge 0.$$$

Lean4

theorem arctan_eq_arccos (h : 0 ≤ x) : arctan x = arccos (√(1 + x ^ 2))⁻¹ :=
  by
  rw [arctan_eq_arcsin, arccos_eq_arcsin]; swap; · exact inv_nonneg.2 (sqrt_nonneg _)
  congr 1
  rw_mod_cast [← sqrt_inv, sq_sqrt, ← one_div, one_sub_div, add_sub_cancel_left, sqrt_div, sqrt_sq h]
  all_goals
    positivity
      -- The junk values for `arccos` and `sqrt` make this true even for `1 < x`.

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