Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-06 19:49 67f36267

View on Github →

feat(data/set/function): ∘ lemmas (#17819) A few lemmas about inj_on/surj_on/bij_on and ∘.

Estimated changes

added theorem equiv.bij_on'
added theorem equiv.bij_on_image
added theorem equiv.bij_on_swap
added theorem equiv.inv_on
added theorem set.bij_on.iterate
added theorem set.bij_on.symm
added theorem set.bij_on_comm
modified theorem set.bij_on_empty
added theorem set.bij_on_id
added theorem set.bij_on_singleton
added theorem set.eq_on_singleton
added theorem set.inj_on.iterate
added theorem set.inj_on_id
added theorem set.inv_on.comp
added theorem set.inv_on_empty
added theorem set.inv_on_id
added theorem set.inv_on_singleton
added theorem set.left_inv_on_empty
added theorem set.left_inv_on_id
added theorem set.maps_to.comp_left
added theorem set.maps_to.comp_right
modified theorem set.maps_to_singleton
added theorem set.right_inv_on_empty
added theorem set.right_inv_on_id
added theorem set.surj_on.comp_left
added theorem set.surj_on.comp_right
added theorem set.surj_on.iterate
added theorem set.surj_on_id
added theorem set.surj_on_singleton