English
There is a FunLike instance on Equiv α β, showing that an equivalence can be viewed as a function with invertibility data.
Русский
Существует экземпляр FunLike на Equiv α β, показывающий, что эквивалентность можно рассматривать как функцию с инвертируемостью.
LaTeX
$$$\\text{Equiv}(\\alpha,\\beta)\\text{ has a }\\operatorname{FunLike} \\text{ instance}. $$$
Lean4
/-- Deprecated helper instance for when inference gets stuck on following the normal chain
`EquivLike → FunLike`. -/
@[deprecated EquivLike.toFunLike (since := "2025-06-20")]
def instFunLike : FunLike (α ≃ β) α β where
coe := Equiv.toFun
coe_injective' := DFunLike.coe_injective
