# Unordered tuples of elements of a list #

Defines `List.sym`

and the specialized `List.sym2`

for computing lists of all unordered n-tuples
from a given list. These are list versions of `Nat.multichoose`

.

## Main declarations #

`List.sym`

:`xs.sym n`

is a list of all unordered n-tuples of elements from`xs`

, with multiplicity. The list's values are in`Sym α n`

.`List.sym2`

:`xs.sym2`

is a list of all unordered pairs of elements from`xs`

, with multiplicity. The list's values are in`Sym2 α`

.

## Todo #

theorem
List.Sublist.sym2
{α : Type u_1}
{xs : List α}
{ys : List α}
(h : List.Sublist xs ys)
:

List.Sublist (List.sym2 xs) (List.sym2 ys)

theorem
List.length_sym2
{α : Type u_1}
{xs : List α}
:

List.length (List.sym2 xs) = Nat.choose (List.length xs + 1) 2

theorem
List.sym2_eq_sym_two
{α : Type u_1}
{xs : List α}
:

List.map (⇑(Sym2.equivSym α)) (List.sym2 xs) = List.sym 2 xs

theorem
List.Sublist.sym
{α : Type u_1}
(n : ℕ)
{xs : List α}
{ys : List α}
(h : List.Sublist xs ys)
:

List.Sublist (List.sym n xs) (List.sym n ys)

theorem
List.sym_sublist_sym_cons
{α : Type u_1}
{xs : List α}
{n : ℕ}
{a : α}
:

List.Sublist (List.sym n xs) (List.sym n (a :: xs))

theorem
List.Nodup.sym
{α : Type u_1}
(n : ℕ)
{xs : List α}
(h : List.Nodup xs)
:

List.Nodup (List.sym n xs)

theorem
List.length_sym
{α : Type u_1}
{n : ℕ}
{xs : List α}
:

List.length (List.sym n xs) = Nat.multichoose (List.length xs) n