mathlib

f06e4e00 - feat(data/sym2) Defining the symmetric square (unordered pairs) (#3264)

feat(data/sym2) Defining the symmetric square (unordered pairs) (#3264) This adds a type for the symmetric square of a type, which is the quotient of the cartesian square by permutations. These are also known as unordered pairs. Additionally, this provides some definitions and lemmas for equalities, functoriality, membership, and a relationship between symmetric relations and terms of the symmetric square. I preferred `sym2` over `unordered_pairs` out of a combination of familiarity and brevity, but I could go either way for naming.