Commit 2024-06-09 17:38 b02cb781

View on Github →

feat(Data/Set/Function): lemmas about inj/bij/surjectivity (#12555) This PR adds a few API lemmas about InjOn, BijOn and SurjOn.

Estimated changes

Modified Mathlib/Data/Set/Function.lean

added theorem Set.BijOn.subset_left

added theorem Set.BijOn.subset_right

added theorem Set.InjOn.image

added theorem Set.InjOn.imageFactorization_injective

added theorem Set.InjOn.image_diff

added theorem Set.InjOn.image_diff_subset

added theorem Set.InjOn.image_eq_image_iff

added theorem Set.InjOn.image_ssubset_image_iff

added theorem Set.InjOn.image_subset_image_iff

added theorem Set.SurjOn.image_invFunOn_image

added theorem Set.SurjOn.image_invFunOn_image_of_subset

added theorem Set.imageFactorization_injective_iff

Modified scripts/style-exceptions.txt