Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-10-02 00:06 e951a752

View on Github →

Merge branch 'master' into master

Estimated changes

Modified data/set/basic.lean

added theorem set.image_preimage_subset

added theorem set.image_subset_eq

added theorem set.image_union_supset

added theorem set.inter_preimage_subset

added theorem set.preimage_diff

added theorem set.subset_preimage_image

added theorem set.union_preimage_subset

Created data/set/function.lean

added theorem set.bij_on.mk

added def set.bij_on

added theorem set.bij_on_comp

added theorem set.bij_on_of_eq_on

added theorem set.bij_on_of_inv_on

added theorem set.bijective_iff_bij_on_univ

added theorem set.eq_on_of_left_inv_of_right_inv

added theorem set.image_eq_of_bij_on

added theorem set.image_eq_of_maps_to_of_surj_on

added theorem set.image_subset_of_maps_to

added theorem set.image_subset_of_maps_to_of_subset

added def set.inj_on

added theorem set.inj_on_comp

added theorem set.inj_on_empty

added theorem set.inj_on_of_bij_on

added theorem set.inj_on_of_eq_on

added theorem set.inj_on_of_inj_on_of_subset

added theorem set.inj_on_of_left_inv_on

added theorem set.injective_iff_inj_on_univ

added def set.inv_on

added def set.left_inv_on

added theorem set.left_inv_on_comp

added theorem set.left_inv_on_of_eq_on_left

added theorem set.left_inv_on_of_eq_on_right

added theorem set.left_inv_on_of_surj_on_right_inv_on

added def set.maps_to

added theorem set.maps_to_comp

added theorem set.maps_to_of_bij_on

added theorem set.maps_to_of_eq_on

added theorem set.maps_to_univ_univ

added def set.right_inv_on

added theorem set.right_inv_on_comp

added theorem set.right_inv_on_of_eq_on_left

added theorem set.right_inv_on_of_eq_on_right

added theorem set.right_inv_on_of_inj_on_of_left_inv_on

added def set.surj_on

added theorem set.surj_on_comp

added theorem set.surj_on_of_bij_on

added theorem set.surj_on_of_eq_on

added theorem set.surj_on_of_right_inv_on

added theorem set.surjective_iff_surj_on_univ