lt_arcsin_iff_sin_lt — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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