Commit 2023-11-10 14:22 508efdc9

View on Github →

feat: two missing injOn lemmas (#8303)

Estimated changes

Modified Mathlib/Data/Set/Function.lean

added theorem Set.exists_image_eq_and_injOn

added theorem Set.exists_image_eq_injOn_of_subset_range

added theorem Set.exists_subset_bijOn

modified theorem Set.surjOn_iff_exists_bijOn_subset