Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-18 19:50 3fcba7d0

View on Github →

feat(logic/basic): add class 'unique' for uniquely inhabited types (#605)

Estimated changes

Modified src/data/equiv/basic.lean

added def equiv.unique_congr

added def equiv.unique_of_equiv

added def equiv_of_unique_of_unique

added def equiv_punit_of_unique

added def unique_unique_equiv

Created src/logic/unique.lean

added theorem unique.default_eq

added theorem unique.eq_default

added def unique.of_surjective

added structure unique