Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-07-06 09:04 d54950a8

View on Github →

refactor(data/subtype): move out of data/sigma/basic.lean

Estimated changes

deleted theorem subtype.coe_eta
deleted theorem subtype.coe_mk
deleted theorem subtype.exists
deleted theorem subtype.ext
deleted theorem subtype.forall
deleted def subtype.map
deleted theorem subtype.map_comp
deleted theorem subtype.map_id
deleted theorem subtype.mk_eq_mk
deleted theorem subtype.val_injective
added theorem subtype.coe_eta
added theorem subtype.coe_mk
added theorem subtype.exists
added theorem subtype.ext
added theorem subtype.forall
added def subtype.map
added theorem subtype.map_comp
added theorem subtype.map_id
added theorem subtype.mk_eq_mk
added theorem subtype.val_injective