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 theorem submodule.coe_eq_coe
modified theorem submodule.mk_eq_zero
modified def dfinsupp.mk
modified theorem dfinsupp.mk_add
modified theorem dfinsupp.mk_apply
added theorem finset.range_coe
deleted theorem finset.range_val
modified theorem hash_map.mk_as_list
modified def hash_map.mk_idx
modified theorem hash_map.mk_valid
modified theorem padic_int.ext
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
deleted theorem vector_space.eval_range
deleted theorem subtype.coe_prop
modified theorem localization_map.mk'_self''
deleted theorem continuous_at_subtype_val
added theorem embedding_subtype_coe
deleted theorem embedding_subtype_val
deleted theorem map_nhds_subtype_val_eq
added theorem isometry_subtype_coe
deleted theorem isometry_subtype_val
modified theorem topological_space.opens.ext
modified theorem compact_iff_compact_univ