le_arcsin_iff_sin_le' — 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,y\in\mathbb{R},\ x\in\left(-\frac{\pi}{2},\frac{\pi}{2}\right),\ y\in[-1,1]\ \Rightarrow\ x \le \arcsin y \iff \sin x \le y$$$

Lean4

theorem le_arcsin_iff_sin_le' {x y : ℝ} (hx : x ∈ Ioc (-(π / 2)) (π / 2)) : x ≤ arcsin y ↔ sin x ≤ y := by
  rw [← neg_le_neg_iff, ← arcsin_neg, arcsin_le_iff_le_sin' ⟨neg_le_neg hx.2, neg_lt.2 hx.1⟩, sin_neg, neg_le_neg_iff]

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