lt_arcsin_iff_sin_lt' — Mathlib

English

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

Русский

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

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 ∈ Ico (-(π / 2)) (π / 2)) : x < arcsin y ↔ sin x < y :=
  not_le.symm.trans <| (not_congr <| arcsin_le_iff_le_sin' hx).trans not_le

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