Commit 2025-07-08 11:47 43a6c4b7

View on Github →

feat(Data/Sym/Sym2): construct set of unordered pairs (#26649) We currently can make the list of unordered pairs from a list, and similarly for multisets and finsets. This PR adds the analogous definition for sets, and adds compatibility lemmas for each of the three above.

Estimated changes

added theorem Finset.coe_sym2
added theorem List.setOf_mem_sym2
added theorem Set.mk'_mem_sym2_iff
added theorem Set.mk_mem_sym2_iff
added theorem Set.mk_preimage_sym2
added def Set.sym2
added theorem Set.sym2_empty
added theorem Set.sym2_eq_mk_image
added theorem Set.sym2_iInter
added theorem Set.sym2_image
added theorem Set.sym2_insert
added theorem Set.sym2_inter
added theorem Set.sym2_preimage
added theorem Set.sym2_singleton
added theorem Set.sym2_univ
added theorem Sym2.coe_mk
added theorem Sym2.map_mk
added theorem Sym2.mk_surjective