Theorems · Definition · combinatorics
Sym2
Type u → Type u
Sym2 α is the symmetric square of α, which, in other words, is the
type of unordered pairs.
It is equivalent in a natural way to multisets of cardinality 2 (see
Sym2.equivMultiset).
- Defined in
- Mathlib.Data.Sym.Sym2
- Cited by
- 737 results in Mathlib
- Foundations
- Depth 2 from the axioms, rests on 3 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Sym2.Relproof · cited by 43
Cited by827
Results whose statement or proof uses this declaration.
- Sym2.mkstatement · cited by 332
- SimpleGraph.edgeSetstatement · cited by 199
- SimpleGraph.Walk.edgesstatement · cited by 145
- SimpleGraph.edgeFinsetstatement · cited by 116
- Sym2.indstatement and proof · cited by 66
- SimpleGraph.deleteEdgesstatement and proof · cited by 64
- Sym2.mapstatement · cited by 61
- SimpleGraph.incidenceSetstatement and proof · cited by 46
- SimpleGraph.fromEdgeSetstatement and proof · cited by 43
- Finset.sym2statement · cited by 43
- Sym2.IsDiagstatement · cited by 43
- Sym2.diagSetstatement and proof · cited by 41
Showing the 200 most cited of 827.