Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-10 11:19 b932a510

View on Github →

feat(data/set/function): add lemmas about semiconj (#3007) Also redefine set.maps_to to avoid unfolding mem_preimage.

Estimated changes

Modified src/analysis/calculus/inverse.lean

Modified src/data/set/function.lean

added theorem function.semiconj.bij_on_image

added theorem function.semiconj.bij_on_range

added theorem function.semiconj.inj_on_image

added theorem function.semiconj.inj_on_preimage

added theorem function.semiconj.inj_on_range

added theorem function.semiconj.maps_to_image

added theorem function.semiconj.maps_to_preimage

added theorem function.semiconj.maps_to_range

added theorem function.semiconj.surj_on_image

added theorem function.semiconj.surj_on_range

modified theorem set.inv_on.bij_on

modified def set.maps_to

Modified src/linear_algebra/basis.lean