English
The sym2 construction for a finite set s is the Finset of all unordered pairs of elements of s, realized as an image of s×s under the quotient to Sym2 α.
Русский
Конструкция sym2 для конечного множества s образует множество неупорядоченных пар элементов s, получаемое как образ произведения s×s в фактор-м множество Sym2 α.
LaTeX
$$The finset ${s}.\text{sym2}$ is the image of $s \times\! s$ under the quotient $\alpha \times \alpha \to \mathrm{Sym}^2(\alpha)$.$$
Lean4
/-- `s.sym2` is the finset of all unordered pairs of elements from `s`.
It is the image of `s ×ˢ s` under the quotient `α × α → Sym2 α`. -/
@[simps]
protected def sym2 (s : Finset α) : Finset (Sym2 α) :=
⟨s.1.sym2, s.2.sym2⟩
