Commit 2021-08-03 11:53 191c247c

View on Github →

feat(Data/Subtype) port data/subtype.lean from mathlib3 (#29)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Subtype.lean

added theorem Subtype.coe_eq_iff

added theorem Subtype.coe_eta

added theorem Subtype.coe_injective

added theorem Subtype.coe_mk

added theorem Subtype.coe_prop

added def Subtype.coind

added theorem Subtype.coind_bijective

added theorem Subtype.coind_injective

added theorem Subtype.coind_surjective

added theorem Subtype.equiv_iff

added theorem Subtype.equivalence

added theorem Subtype.ext_iff

added theorem Subtype.ext_iff_val

added theorem Subtype.ext_val

added theorem Subtype.heq_iff_coe_eq

added theorem Subtype.heq_iff_coe_heq

added def Subtype.map

added theorem Subtype.map_comp

added theorem Subtype.map_id

added theorem Subtype.map_injective

added theorem Subtype.map_involutive

added theorem Subtype.mk_eq_mk

added theorem Subtype.prop

added def Subtype.restrict

added theorem Subtype.restrict_apply

added theorem Subtype.restrict_def

added theorem Subtype.restrict_injective

added def Subtype.simps.coe

added theorem Subtype.val_eq_coe

added theorem Subtype.val_injective

added theorem Subtype.val_prop

Modified Mathlib/Logic/Basic.lean

added theorem heq_iff_eq