mathlib

cabb8aee - refactor(data/finset/image): split out of data/finset/basic (#17852)

refactor(data/finset/image): split out of data/finset/basic (#17852) This somewhat matches the split for `data/set/basic`, and makes the file shorter by a reasonable amount. The proof of `bUnion_singleton_eq_self` was tweaked slightly so that it didn't need to move file.