arcsin_eq_of_sin_eq — Mathlib

English

If sin x = y and x ∈ [−π/2, π/2], then arcsin y = x.

Русский

Если sin x = y и x ∈ [−π/2, π/2], то arcsin y = x.

LaTeX

$$$\\sin x = y \\Rightarrow \\left( x \\in [-\\frac{\\pi}{2}, \\frac{\\pi}{2}] \\Rightarrow \\arcsin y = x \\right)$$$

Lean4

theorem arcsin_eq_of_sin_eq {x y : ℝ} (h₁ : sin x = y) (h₂ : x ∈ Icc (-(π / 2)) (π / 2)) : arcsin y = x :=
  by
  subst y
  exact injOn_sin (arcsin_mem_Icc _) h₂ (sin_arcsin' (sin_mem_Icc x))

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