Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-28 06:01 a220286a

View on Github →

feat(subtype): standardize (#3204) Add simp lemma from x.val to coe x Use correct ext/ext_iff naming scheme Use coe in more places in the library

Estimated changes

modified def dfinsupp.mk
modified theorem dfinsupp.mk_add
modified theorem dfinsupp.mk_apply
deleted theorem set.range_coe_subtype
added theorem set.set_of_set
added theorem subtype.coe_image
added theorem subtype.coe_image_univ
modified theorem subtype.image_preimage_val
modified theorem subtype.mem
added theorem subtype.range_coe
modified theorem subtype.range_val
deleted theorem subtype.val_image
deleted theorem subtype.val_image_subset
deleted theorem subtype.val_image_univ
deleted theorem subtype.val_range
modified theorem subtype.coe_eta
deleted theorem subtype.coe_ext
added theorem subtype.coe_injective
modified theorem subtype.coe_mk
added theorem subtype.coe_prop
deleted theorem subtype.exists
deleted theorem subtype.ext
added theorem subtype.ext_iff
added theorem subtype.ext_iff_val
added theorem subtype.ext_val
deleted theorem subtype.forall'
deleted theorem subtype.forall
modified theorem subtype.mk_eq_mk
added theorem subtype.prop
modified theorem subtype.restrict_def
modified theorem subtype.val_eq_coe
deleted theorem subtype.val_prop'
modified theorem subtype.val_prop