arcsin_le_iff_le_sin — Mathlib

English

For x ∈ [−1,1] and y ∈ [−π/2, π/2], arcsin x ≤ y if and only if x ≤ sin y.

Русский

Для x ∈ [−1,1] и y ∈ [−π/2, π/2], arcsin x ≤ y тогда и только тогда, когда x ≤ sin y.

LaTeX

$$$\\text{if } x \\in [-1,1] \\text{ and } y \\in [-\\frac{\\pi}{2}, \\frac{\\pi}{2}], \\ arcsin x \\le y \\Leftrightarrow x \\le \\sin y$$$

Lean4

theorem arcsin_le_iff_le_sin {x y : ℝ} (hx : x ∈ Icc (-1 : ℝ) 1) (hy : y ∈ Icc (-(π / 2)) (π / 2)) :
    arcsin x ≤ y ↔ x ≤ sin y := by
  rw [← arcsin_sin' hy, strictMonoOn_arcsin.le_iff_le hx (sin_mem_Icc _), arcsin_sin' hy]

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