Commit 2022-11-07 03:29 a1af1761

View on Github →

feat: port Data.Subtype (#546)

Estimated changes

Modified Mathlib/Data/Subtype.lean

added def Subtype.Simps.coe

modified theorem Subtype.coe_eq_iff

added theorem Subtype.coe_eq_of_eq_mk

modified theorem Subtype.coe_eta

added theorem Subtype.coe_inj

modified theorem Subtype.coe_injective

modified theorem Subtype.coe_mk

added theorem Subtype.coe_prop

modified def Subtype.coind

modified theorem Subtype.coind_bijective

modified theorem Subtype.coind_injective

modified theorem Subtype.coind_surjective

modified theorem Subtype.equiv_iff

modified theorem Subtype.ext_iff

modified theorem Subtype.ext_iff_val

modified theorem Subtype.ext_val

modified theorem Subtype.heq_iff_coe_eq

modified def Subtype.map

modified theorem Subtype.map_id

modified theorem Subtype.map_injective

modified theorem Subtype.map_involutive

modified theorem Subtype.prop

modified def Subtype.restrict

modified theorem Subtype.restrict_apply

modified theorem Subtype.restrict_def

modified theorem Subtype.restrict_injective

deleted def Subtype.simps.coe

added theorem Subtype.surjective_restrict

added theorem Subtype.val_inj

modified theorem Subtype.val_prop

added theorem exists_eq_subtype_mk_iff

added theorem exists_subtype_mk_eq_iff