Mathlib v3 is deprecated. Go to Mathlib v4

Theorem function.bijective_iff_exists_unique

Modification history

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_iff_exists_unique View on Github →