Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-06-12 22:37 3c554a34

View on Github →

refactor(data/equiv): move subtype.map

Estimated changes

Modified data/equiv.lean

modified def equiv.decidable_eq_of_equiv

modified def equiv.inhabited_of_equiv

deleted def subtype.map

deleted theorem subtype.map_comp

deleted theorem subtype.map_id

Modified data/sigma/basic.lean

added def subtype.map

added theorem subtype.map_comp

added theorem subtype.map_id