Commit 2024-03-03 21:54 52762e24

View on Github →

feat(Set): API for subset restriction and coercion to/from subtypes (#9940) Api for subset restriction and coercion to/from subtypes

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Set/Functor.lean

added def Set.Notation.delab_set_image_subtype

Modified Mathlib/Data/Set/Image.lean

added theorem Subtype.preimage_val_subset_preimage_val_iff

Created Mathlib/Data/Set/Subset.lean

added theorem Set.cou_inter_self_right_eq_coe

added theorem Set.eq_of_preimage_val_eq_of_subset

added theorem Set.image_val_compl

added theorem Set.image_val_diff

added theorem Set.image_val_iInter

added theorem Set.image_val_iUnion

added theorem Set.image_val_inj

added theorem Set.image_val_injective

added theorem Set.image_val_inter

added theorem Set.image_val_inter_self_left_eq_coe

added theorem Set.image_val_mono

added theorem Set.image_val_preimage_val_subset_self

added theorem Set.image_val_sInter

added theorem Set.image_val_sUnion

added theorem Set.image_val_union

added theorem Set.image_val_union_self_left_eq

added theorem Set.image_val_union_self_right_eq

added theorem Set.preimage_val_eq_univ_of_subset

added theorem Set.preimage_val_iInter

added theorem Set.preimage_val_image_val_eq_self

added theorem Set.preimage_val_sInter

added theorem Set.preimage_val_sInter_eq_sInter

added theorem Set.preimage_val_sUnion

added theorem Set.subset_of_image_val_subset_image_val

added theorem Set.subset_preimage_val_image_val_iff