Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-10-15 02:26 5ad8020f

View on Github →

Merge remote-tracking branch 'minchaowu/master'

Estimated changes

Modified analysis/real.lean

Modified analysis/topology/continuity.lean

Modified analysis/topology/infinite_sum.lean

Modified analysis/topology/uniform_space.lean

Modified data/set/basic.lean

added theorem set.image_subset_iff

deleted theorem set.image_subset_iff_subset_preimage

added theorem set.inter_preimage_subset

added theorem set.preimage_diff

added theorem set.subset_image_union

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

Modified order/filter.lean

Modified order/galois_connection.lean