le_arcsin_iff_sin_le — Mathlib

English

If x ∈ [−π/2, π/2] and y ∈ [−1, 1], then x ≤ arcsin y if and only if 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 ∈ Icc (-(π / 2)) (π / 2)) (hy : y ∈ Icc (-1 : ℝ) 1) :
    x ≤ arcsin y ↔ sin x ≤ y := by
  rw [← neg_le_neg_iff, ← arcsin_neg,
    arcsin_le_iff_le_sin ⟨neg_le_neg hy.2, neg_le.2 hy.1⟩ ⟨neg_le_neg hx.2, neg_le.2 hx.1⟩, sin_neg, neg_le_neg_iff]

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