Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-08 06:17 ec514603

View on Github →

feat(data/finset): define finset.pimage (#8907)

Estimated changes

added theorem finset.coe_pimage
added theorem finset.mem_pimage
added def finset.pimage
added theorem finset.pimage_congr
added theorem finset.pimage_empty
added theorem finset.pimage_inter
added theorem finset.pimage_mono
added theorem finset.pimage_some
added theorem finset.pimage_subset
added theorem finset.pimage_union
added theorem part.coe_to_finset
added theorem part.mem_to_finset
added def part.to_finset
added theorem part.to_finset_none
added theorem part.to_finset_some
added theorem part.bind_of_mem
added theorem part.eq_get_iff_mem
added theorem part.get_eq_iff_mem
modified theorem part.get_or_else_none
modified theorem part.get_or_else_some
modified def part.map
added theorem part.none_ne_some
added theorem part.none_to_option
modified def part.restrict
modified theorem part.some_ne_none
added theorem part.some_to_option
added theorem and.exists