equiv.surjective

Stream: general

[Sebastien Gouezel]

I can not find the fact that an equiv is surjective:

example {E : Type} (e : equiv E E) : function.surjective e :=
by library_search

fails. There is the fact that it is bijective, though. Would it be reasonable to add explicitly to the library statements about surjectivity and injectivity of equivs?

[Mario Carneiro]

I use e.bijective.1 and e.bijective.2

[Mario Carneiro]

because I was too lazy to just add the theorems

[Sebastien Gouezel]

That's what I ended up doing, but I think these statements are so important that they're worth adding. I'll do it.

[Kevin Buzzard]

I had this experience only last week, and was also surprised.