mathlib
407d1386 - chore(category_theory/equivalence): weaken essential surjectivity (#3821)

Commit

5 years ago

chore(category_theory/equivalence): weaken essential surjectivity (#3821) Weaken essential surjectivity to be a Prop, rather than the data of the inverse.

Author

b-mehta

Parents

a1aa5110

mathlib 407d1386 - chore(category_theory/equivalence): weaken essential surjectivity (#3821)

mathlib
407d1386 - chore(category_theory/equivalence): weaken essential surjectivity (#3821)