arcsin_le_iff_le_sin' — Mathlib

English

Let y be in the interval [−π/2, π/2) and x be any real number. Then arcsin x ≤ y if and only if x ≤ sin y.

Русский

Пусть y принадлежит интервалу [−π/2, π/2) и x — произвольное число. Тогда arcsin x ≤ y тогда и только тогда, когда x ≤ sin y.

LaTeX

$$$\forall x \in \mathbb{R},\ \forall y \in \left[-\frac{\pi}{2}, \frac{\pi}{2}\right)\; \arcsin x \le y \iff x \le \sin y$$$

Lean4

theorem arcsin_le_iff_le_sin' {x y : ℝ} (hy : y ∈ Ico (-(π / 2)) (π / 2)) : arcsin x ≤ y ↔ x ≤ sin y :=
  by
  rcases le_total x (-1) with hx₁ | hx₁
  · simp [arcsin_of_le_neg_one hx₁, hy.1, hx₁.trans (neg_one_le_sin _)]
  rcases lt_or_ge 1 x with hx₂ | hx₂
  · simp [arcsin_of_one_le hx₂.le, hy.2.not_ge, (sin_le_one y).trans_lt hx₂]
  exact arcsin_le_iff_le_sin ⟨hx₁, hx₂⟩ (mem_Icc_of_Ico hy)

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