Commit 2023-12-15 13:12 d08e3e0d

View on Github →

feat(Set/Lattice): add Set.seq_eq_image2, use it to golf some proofs (#9062)

Estimated changes

modified theorem Set.iUnion_image_right
modified theorem Set.seq_def
added theorem Set.seq_eq_image2
modified theorem Set.seq_singleton
modified theorem Set.singleton_seq