English
Any F with EquivLike F α β can be turned into an actual Equiv α β via toEquiv: toEquiv(f) is the Equiv corresponding to f with toFun = f and appropriate inverses.
Русский
Любой F с EquivLike F α β можно привести к действительной эквивалентности α β с помощью toEquiv; toEquiv(f) задаёт эквивалентность с toFun = f и нужными обратными.
LaTeX
$$$\\operatorname{toEquiv}(f) : \\alpha \\simeq \\beta.$$$
Lean4
/-- Turn an element of a type `F` satisfying `EquivLike F α β` into an actual
`Equiv`. This is declared as the default coercion from `F` to `α ≃ β`. -/
@[coe]
def toEquiv {F} [EquivLike F α β] (f : F) : α ≃ β where
toFun := f
invFun := EquivLike.inv f
left_inv := EquivLike.left_inv f
right_inv := EquivLike.right_inv f
