English
The sine function, with arcsin as inverse, forms an open partial homeomorphism between the interval (−π/2, π/2) and the interval (−1, 1).
Русский
Функция синуса, имеющая обратную дуг Sinclair arcsin в качестве обратной, образует открытый частичный гомоморфизм между интервалами (−π/2, π/2) и (−1, 1).
LaTeX
$$$\text{sinPartialHomeomorph} : \text{OpenPartialHomeomorph}(\mathbb{R}, \mathbb{R})\, ,\
toFun = \sin,\ invFun = \arcsin,\ source = (-\tfrac{\pi}{2},\ \tfrac{\pi}{2}),\ target = (-1,1)$$$
Lean4
/-- `Real.sin` as an `OpenPartialHomeomorph` between `(-π / 2, π / 2)` and `(-1, 1)`. -/
@[simp]
def sinPartialHomeomorph : OpenPartialHomeomorph ℝ ℝ
where
toFun := sin
invFun := arcsin
source := Ioo (-(π / 2)) (π / 2)
target := Ioo (-1) 1
map_source' := mapsTo_sin_Ioo
map_target' _ hy := ⟨neg_pi_div_two_lt_arcsin.2 hy.1, arcsin_lt_pi_div_two.2 hy.2⟩
left_inv' _ hx := arcsin_sin hx.1.le hx.2.le
right_inv' _ hy := sin_arcsin hy.1.le hy.2.le
open_source := isOpen_Ioo
open_target := isOpen_Ioo
continuousOn_toFun := continuous_sin.continuousOn
continuousOn_invFun := continuous_arcsin.continuousOn
