English
The tangent function provides an open partial homeomorphism between (-π/2, π/2) and ℝ with arctan as its inverse.
Русский
Тангенс задаёт открытую частичную гомоморфию между (-π/2, π/2) и ℝ с обратной функцией arctan.
LaTeX
$$$\\text{tanPartialHomeomorph}: \\text{OpenPartialHomeomorph}(\\\\mathbb{R},\\\\mathbb{R})$ with toFun $= \\\\tan$, invFun $= \\\\arctan$, source $=(-\\\\frac{\\\\pi}{2},\\\\frac{\\\\pi}{2})$, target $\\\\mathbb{R}$, left_inv$=\\\\arctan \\\\tan$, right_inv$=\\\\tan \\\\arctan$.$$
Lean4
/-- `Real.tan` as an `OpenPartialHomeomorph` between `(-(π / 2), π / 2)` and the whole line. -/
def tanPartialHomeomorph : OpenPartialHomeomorph ℝ ℝ
where
toFun := tan
invFun := arctan
source := Ioo (-(π / 2)) (π / 2)
target := univ
map_source' := mapsTo_univ _ _
map_target' y _ := arctan_mem_Ioo y
left_inv' _ hx := arctan_tan hx.1 hx.2
right_inv' y _ := tan_arctan y
open_source := isOpen_Ioo
open_target := isOpen_univ
continuousOn_toFun := continuousOn_tan_Ioo
continuousOn_invFun := continuous_arctan.continuousOn
