inverse function from bijection

Stream: general

[Bernd Losert]

How do you get the inverse function from function.bijective f?

[Eric Wieser]

docs#function.inv_fun?

[Eric Wieser]

or maybe docs#function.surj_inv

[Bernd Losert]

Nice. Thank you.

[Adam Topaz]

You can even build an equiv using docs#equiv.of_bijective

[Bernd Losert]

Cool.

[Kevin Buzzard]

Remember it's noncomputable though (not that we're too bothered about this around here!)

[Adam Topaz]

That's right. That means it can be slightly tedious to prove things involving the inverse if you need to use the precise definition of your function.

[Eric Wieser]

It might be better to just work with docs#equiv instead of bijective in the first place

[Yury G. Kudryashov]

BTW, should we have can_lift (α → β) (α ≃ β) with cond := bijective (and probably same for embedding and injective)? Or should we wait till someone needs it in a tactic proof?

[Eric Wieser]

I don't think those are urgent, but if someone spends the time to PR them I see no harm in adding them

[Yaël Dillies]

You mean embedding + surjective, I assume?

[Yury G. Kudryashov]

I meant can_lift (α → β) (α ↪ β) with cond := injective.