sin_arccos — Mathlib

English

For every real x, sin(arccos x) = sqrt(1 - x^2).

Русский

Пусть x ∈ ℝ. Тогда sin(arccos x) = √(1 - x^2).

LaTeX

$$\n sin(\arccos x) = \sqrt{1 - x^2}$$

Lean4

theorem sin_arccos (x : ℝ) : sin (arccos x) = √(1 - x ^ 2) :=
  by
  by_cases hx₁ : -1 ≤ x; swap
  · rw [not_le] at hx₁
    rw [arccos_of_le_neg_one hx₁.le, sin_pi, sqrt_eq_zero_of_nonpos]
    nlinarith
  by_cases hx₂ : x ≤ 1; swap
  · rw [not_le] at hx₂
    rw [arccos_of_one_le hx₂.le, sin_zero, sqrt_eq_zero_of_nonpos]
    nlinarith
  rw [arccos_eq_pi_div_two_sub_arcsin, sin_pi_div_two_sub, cos_arcsin]

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