English
Any isomorphism i: X ≅ Y gives a bijection X ≃ Y by defining the equivalence with toFun = i.hom and invFun = i.inv, and left/right inverses given by i.hom_inv_id and i.inv_hom_id.
Русский
Любой изоморфизм i: X ≅ Y задаёт биекцию X ≃ Y, где отображение вперёд задано i.hom, обратное — i.inv, а левый/правый обратные — i.hom_inv_id и i.inv_hom_id.
LaTeX
$$$ (i : X \\cong Y) \\Rightarrow (i.toEquiv : X \\simeq Y) \\text{ с } (i.toEquiv)(x)=i.hom(x),\\ (i.toEquiv)^{-1}(y)=i.inv(y) $$$
Lean4
/-- Any isomorphism between types gives an equivalence. -/
def toEquiv (i : X ≅ Y) : X ≃ Y where
toFun := i.hom
invFun := i.inv
left_inv x := congr_fun i.hom_inv_id x
right_inv y := congr_fun i.inv_hom_id y
