English
If a right inverse g of f is given, there exists a homeomorphism with forward map f and inverse map g.
Русский
Если задана правая обратная функция g к f, существует гомеоморфизм с прямым отображением f и обратной картой g.
LaTeX
$$$\\exists h:\\, X\\simeq Y,\\ h=f\\land h^{-1}=g$$$
Lean4
/-- Change the homeomorphism `f` to make the inverse function definitionally equal to `g`. -/
def changeInv (f : X ≃ₜ Y) (g : Y → X) (hg : Function.RightInverse g f) : X ≃ₜ Y :=
haveI : g = f.symm := (f.left_inv.eq_rightInverse hg).symm
{ toFun := f
invFun := g
left_inv := by convert f.left_inv
right_inv := by convert f.right_inv using 1
continuous_toFun := f.continuous
continuous_invFun := by convert f.symm.continuous }
