mapsTo_sin_Ioo — Mathlib

English

Sin maps the open interval (−π/2, π/2) into the open interval (−1, 1).

Русский

Sin отображает открытый интервал (−π/2, π/2) в открытый интервал (−1, 1).

LaTeX

$$$\text{MapsTo}(\sin,\, (-\tfrac{\pi}{2}, \tfrac{\pi}{2}), (-1,1))$$$

Lean4

theorem mapsTo_sin_Ioo : MapsTo sin (Ioo (-(π / 2)) (π / 2)) (Ioo (-1) 1) := fun x h => by
  rwa [mem_Ioo, ← arcsin_lt_pi_div_two, ← neg_pi_div_two_lt_arcsin, arcsin_sin h.1.le h.2.le]

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