Mathlib v3 is deprecated. Go to Mathlib v4

Theorem function.bijective.exists_unique

Modification history

2021-11-16 08:37
src/logic/function/basic.lean
feat(algebra/order/archimedean): upgrade some `∃` to `∃!` (#10343)
Deleted function.bijective.exists_uniqueView on Github →
2021-02-02 14:43
src/logic/function/basic.lean
feat(logic/function/basic): add bijective.iff_exists_unique and projections (#5995)
Added function.bijective.exists_uniqueView on Github →