tan_arcsin — Mathlib

English

For all x with -1 ≤ x ≤ 1, tan(arcsin x) = x / √(1 - x^2).

Русский

Для всех x с -1 ≤ x ≤ 1: tan(arcsin x) = x / √(1 - x^2).

LaTeX

$$$-1 \le x \le 1 \Rightarrow \tan(\arcsin x) = \dfrac{x}{\sqrt{1 - x^2}}$$$

Lean4

theorem tan_arcsin (x : ℝ) : tan (arcsin x) = x / √(1 - x ^ 2) :=
  by
  rw [tan_eq_sin_div_cos, cos_arcsin]
  by_cases hx₁ : -1 ≤ x; swap
  · have h : √(1 - x ^ 2) = 0 := sqrt_eq_zero_of_nonpos (by nlinarith)
    rw [h]
    simp
  by_cases hx₂ : x ≤ 1; swap
  · have h : √(1 - x ^ 2) = 0 := sqrt_eq_zero_of_nonpos (by nlinarith)
    rw [h]
    simp
  rw [sin_arcsin hx₁ hx₂]

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