Mathlib v3 is deprecated. Go to Mathlib v4

Theorem function.surjective.exists

Modification history

2021-11-16 08:37
src/logic/function/basic.lean
feat(algebra/order/archimedean): upgrade some `∃` to `∃!` (#10343)
Deleted function.surjective.existsView on Github →
2020-07-06 05:41
src/logic/function/basic.lean
refactor(algebra/inj_surj): more lemmas, move to files, rename (#3290) …
Added function.surjective.existsView on Github →