English
A local homeomorphism exists on (0, ∞) between itself with square and square root as inverse.
Русский
Существует локальный гомоморфизм между (0, ∞) и самим собой, заданный переходом x ↦ x^2 и обратной функцией sqrt.
LaTeX
$$$$ \text{OpenPartialHomeomorph }(0, \infty) \to (0, \infty) \text{ with } x \mapsto x^2 \text{ and } y \mapsto \sqrt{y}. $$$$
Lean4
/-- Local homeomorph between `(0, +∞)` and `(0, +∞)` with `toFun = (· ^ 2)` and
`invFun = Real.sqrt`. -/
noncomputable def sqPartialHomeomorph : OpenPartialHomeomorph ℝ ℝ
where
toFun x := x ^ 2
invFun := (√·)
source := Ioi 0
target := Ioi 0
map_source' _ h := mem_Ioi.2 (pow_pos (mem_Ioi.1 h) _)
map_target' _ h := mem_Ioi.2 (sqrt_pos.2 h)
left_inv' _ h := sqrt_sq (le_of_lt h)
right_inv' _ h := sq_sqrt (le_of_lt h)
open_source := isOpen_Ioi
open_target := isOpen_Ioi
continuousOn_toFun := (continuous_pow 2).continuousOn
continuousOn_invFun := continuousOn_id.sqrt
