Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-13 22:27 db1c5001

View on Github →

refactor(data/set/function): use dot notation (#1934)

Estimated changes

Modified src/data/equiv/local_equiv.lean

Modified src/data/finsupp.lean

Modified src/data/set/basic.lean

deleted def set.eq_on

deleted theorem set.image_eq_image_of_eq_on

Modified src/data/set/countable.lean

Modified src/data/set/finite.lean

Modified src/data/set/function.lean

added theorem function.injective.comp_inj_on

added theorem function.injective.inj_on

added theorem function.surjective.surj_on

added theorem set.bij_on.comp

added theorem set.bij_on.congr

added theorem set.bij_on.image_eq

added theorem set.bij_on.inj_on

added theorem set.bij_on.inv_on_inv_fun_on

added theorem set.bij_on.maps_to

modified theorem set.bij_on.mk

added theorem set.bij_on.surj_on

modified def set.bij_on

deleted theorem set.bij_on_comp

added theorem set.bij_on_empty

deleted theorem set.bij_on_of_eq_on

deleted theorem set.bij_on_of_inv_on

modified theorem set.bijective_iff_bij_on_univ

added theorem set.eq_on.bij_on_iff

added theorem set.eq_on.image_eq

added theorem set.eq_on.inj_on_iff

added theorem set.eq_on.maps_to_iff

added theorem set.eq_on.mono

added theorem set.eq_on.surj_on_iff

added theorem set.eq_on.symm

added theorem set.eq_on.trans

added def set.eq_on

added theorem set.eq_on_comm

modified theorem set.eq_on_of_left_inv_of_right_inv

added theorem set.eq_on_refl

deleted theorem set.image_eq_of_bij_on

deleted theorem set.image_eq_of_maps_to_of_surj_on

deleted theorem set.image_subset_of_maps_to

deleted theorem set.image_subset_of_maps_to_of_subset

added theorem set.inj_on.bij_on_image

added theorem set.inj_on.comp

added theorem set.inj_on.congr

added theorem set.inj_on.inv_fun_on_image

added theorem set.inj_on.left_inv_on_inv_fun_on

added theorem set.inj_on.mono

added theorem set.inj_on.right_inv_on_of_left_inv_on

deleted theorem set.inj_on.to_bij_on

modified def set.inj_on

deleted theorem set.inj_on_comp

deleted theorem set.inj_on_comp_of_injective_left

modified theorem set.inj_on_iff_injective

deleted theorem set.inj_on_of_bij_on

deleted theorem set.inj_on_of_eq_on

deleted theorem set.inj_on_of_inj_on_of_subset

deleted theorem set.inj_on_of_injective

deleted theorem set.inj_on_of_left_inv_on

modified theorem set.inj_on_preimage

modified theorem set.injective_iff_inj_on_univ

deleted theorem set.inv_fun_on_image

added theorem set.inv_on.bij_on

added theorem set.inv_on.symm

modified def set.inv_on

added theorem set.left_inv_on.comp

added theorem set.left_inv_on.congr_left

added theorem set.left_inv_on.congr_right

added theorem set.left_inv_on.eq

added theorem set.left_inv_on.eq_on

added theorem set.left_inv_on.inj_on

added theorem set.left_inv_on.surj_on

modified def set.left_inv_on

deleted theorem set.left_inv_on_comp

deleted theorem set.left_inv_on_of_eq_on_left

deleted theorem set.left_inv_on_of_eq_on_right

deleted theorem set.left_inv_on_of_surj_on_right_inv_on

modified theorem set.maps_to'

added theorem set.maps_to.comp

added theorem set.maps_to.congr

added theorem set.maps_to.image_subset

added theorem set.maps_to.mono

modified def set.maps_to

deleted theorem set.maps_to_comp

added theorem set.maps_to_empty

modified theorem set.maps_to_image

deleted theorem set.maps_to_of_bij_on

deleted theorem set.maps_to_of_eq_on

added theorem set.maps_to_preimage

modified theorem set.maps_to_range

modified theorem set.maps_to_univ

modified theorem set.range_restrict

added theorem set.right_inv_on.comp

added theorem set.right_inv_on.congr_left

added theorem set.right_inv_on.congr_right

added theorem set.right_inv_on.eq

added theorem set.right_inv_on.eq_on

added theorem set.right_inv_on.surj_on

modified def set.right_inv_on

deleted theorem set.right_inv_on_comp

deleted theorem set.right_inv_on_of_eq_on_left

deleted theorem set.right_inv_on_of_eq_on_right

deleted theorem set.right_inv_on_of_inj_on_of_left_inv_on

deleted theorem set.subset_image_iff

deleted theorem set.subset_range_iff

added theorem set.surj_on.bij_on_subset

added theorem set.surj_on.comap_nonempty

added theorem set.surj_on.comp

added theorem set.surj_on.congr

added theorem set.surj_on.image_eq_of_maps_to

added theorem set.surj_on.inv_on_inv_fun_on

added theorem set.surj_on.left_inv_on_of_right_inv_on

added theorem set.surj_on.maps_to_inv_fun_on

added theorem set.surj_on.mono

added theorem set.surj_on.right_inv_on_inv_fun_on

modified def set.surj_on

deleted theorem set.surj_on_comp

added theorem set.surj_on_empty

added theorem set.surj_on_iff_exists_bij_on_subset

modified theorem set.surj_on_iff_surjective

deleted theorem set.surj_on_of_bij_on

deleted theorem set.surj_on_of_eq_on

deleted theorem set.surj_on_of_right_inv_on

modified theorem set.surjective_iff_surj_on_univ

Modified src/data/subtype.lean

Modified src/linear_algebra/basis.lean

Modified src/topology/continuous_on.lean

Modified src/topology/metric_space/closeds.lean

Modified src/topology/uniform_space/uniform_embedding.lean