bijection

Stream: Is there code for X?

[Bolton Bailey]

I thought mathlib had an object for a "bijection": a function wrapped with a function.bijective predicate. But searching for it in the docs yields no results. Do we have this?

[Bolton Bailey]

Similarly, I thought we had wrapped injections and surjections with funny little arrow symbols as notation, do we not have this either?

[Junyan Xu]

For injection we have docs#embedding but not sure about others

[Junyan Xu]

sorry, docs#function.embedding with notation ↪

[Junyan Xu]

docs#equiv is sort of bundled bijection but has the additional data of the inverse function, and is what people normally use.

[Bolton Bailey]

Embedding must have been what I saw, thanks

[Junyan Xu]

because we always have docs#equiv.of_bijective using choice (in ZF it doesn't require choice but in Lean it does).