arcsin_lt_iff_lt_sin — Mathlib

English

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

Русский

Если x ∈ [−1,1] и y ∈ [−π/2, π/2], тогда arcsin x < y тогда и только тогда, когда x < sin y.

LaTeX

$$$\forall x\in[-1,1],\forall y\in\left[-\frac{\pi}{2},\frac{\pi}{2}\right],\ arcin x < y \iff x < \sin y$$$

Lean4

theorem arcsin_lt_iff_lt_sin {x y : ℝ} (hx : x ∈ Icc (-1 : ℝ) 1) (hy : y ∈ Icc (-(π / 2)) (π / 2)) :
    arcsin x < y ↔ x < sin y :=
  not_le.symm.trans <| (not_congr <| le_arcsin_iff_sin_le hy hx).trans not_le

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