arcsin_eq_iff_eq_sin — Mathlib

English

If y ∈ (−π/2, π/2), then arcsin x = y iff x = sin y.

Русский

Если y ∈ (−π/2, π/2), тогда arcsin x = y эквивалентно x = sin y.

LaTeX

$$$\forall x,y\in\mathbb{R},\ y\in\left(-\frac{\pi}{2},\frac{\pi}{2}\right)\Rightarrow\ arcsin x = y \iff x = \sin y$$$

Lean4

theorem arcsin_eq_iff_eq_sin {x y : ℝ} (hy : y ∈ Ioo (-(π / 2)) (π / 2)) : arcsin x = y ↔ x = sin y := by
  simp only [le_antisymm_iff, arcsin_le_iff_le_sin' (mem_Ico_of_Ioo hy), le_arcsin_iff_sin_le' (mem_Ioc_of_Ioo hy)]

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