arctan_eq_arcsin — Mathlib

English

For every real x, arctan x equals arcsin of x divided by the square root of (1 plus x^2).

Русский

Пусть для каждого действительного x выполняется arctan x = arcsin( x / √(1 + x^2) ).

LaTeX

$$$\\forall x \\in \\mathbb{R}, \\arctan x = \\arcsin \\left( \\frac{x}{\\sqrt{1 + x^2}} \\right)$$$

Lean4

theorem arctan_eq_arcsin (x : ℝ) : arctan x = arcsin (x / √(1 + x ^ 2)) :=
  Eq.symm <| arcsin_eq_of_sin_eq (sin_arctan x) (mem_Icc_of_Ioo <| arctan_mem_Ioo x)

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