Commit 2025-01-03 11:02 3997f6f5

View on Github →

feat: f '' sᶜ = range f \ f '' s when f is injective (#19030) From GrowthInGroups (LeanCamCombi)

Estimated changes

Modified Mathlib/Data/Set/Image.lean

added theorem Set.image_compl_eq_range_diff_image

modified theorem Set.range_diff_image