Commit 2022-12-07 20:30 1b36dabc
View on Github →refactor(data/set/basic): move image, preimage, and range to a new file (#17842)
This means data.set.basic
is mainly about lattice operations.
Only one proof is modified (to avoid it needing to move between files). All other lemmas are copied verbatim.