Commit 2022-12-08 18:41 cabb8aee
View on Github →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.