# Documentation

Mathlib.Data.List.Sym

# 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 #

• Prove protected theorem Perm.sym (n : ℕ) {xs ys : List α} (h : xs ~ ys) : xs.sym n ~ ys.sym n and lift the result to Multiset and Finset.
def List.sym2 {α : Type u_1} :
List αList (Sym2 α)

xs.sym2 is a list of all unordered pairs of elements from xs. If xs has no duplicates then neither does xs.sym2.

Equations
Instances For
theorem List.mem_sym2_cons_iff {α : Type u_1} {x : α} {xs : List α} {z : Sym2 α} :
z List.sym2 (x :: xs) z = (x, x) (∃ y ∈ xs, z = (x, y)) z
@[simp]
theorem List.sym2_eq_nil_iff {α : Type u_1} {xs : List α} :
= [] xs = []
theorem List.left_mem_of_mk_mem_sym2 {α : Type u_1} {xs : List α} {a : α} {b : α} (h : (a, b) ) :
a xs
theorem List.right_mem_of_mk_mem_sym2 {α : Type u_1} {xs : List α} {a : α} {b : α} (h : (a, b) ) :
b xs
theorem List.mk_mem_sym2 {α : Type u_1} {xs : List α} {a : α} {b : α} (ha : a xs) (hb : b xs) :
(a, b)
theorem List.mk_mem_sym2_iff {α : Type u_1} {xs : List α} {a : α} {b : α} :
(a, b) a xs b xs
theorem List.mem_sym2_iff {α : Type u_1} {xs : List α} {z : Sym2 α} :
z yz, y xs
theorem List.Nodup.sym2 {α : Type u_1} {xs : List α} (h : ) :
theorem List.Perm.sym2 {α : Type u_1} {xs : List α} {ys : List α} (h : xs ~ ys) :
~
theorem List.Sublist.sym2 {α : Type u_1} {xs : List α} {ys : List α} (h : List.Sublist xs ys) :
theorem List.Subperm.sym2 {α : Type u_1} {xs : List α} {ys : List α} (h : xs <+~ ys) :
<+~
theorem List.length_sym2 {α : Type u_1} {xs : List α} :
def List.sym {α : Type u_1} (n : ) :
List αList (Sym α n)

xs.sym n is all unordered n-tuples from the list xs in some order.

Equations
Instances For
theorem List.sym_one_eq {α : Type u_1} {xs : List α} :
List.sym 1 xs = List.map (fun (x : α) => x ::ₛ Sym.nil) xs
theorem List.sym2_eq_sym_two {α : Type u_1} {xs : List α} :
List.map (()) () = List.sym 2 xs
theorem List.sym_map {α : Type u_1} {β : Type u_2} (f : αβ) (n : ) (xs : List α) :
List.sym n (List.map f xs) = List.map () (List.sym n xs)
theorem List.Sublist.sym {α : Type u_1} (n : ) {xs : List α} {ys : List α} (h : List.Sublist xs 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.mem_of_mem_of_mem_sym {α : Type u_1} {n : } {xs : List α} {a : α} {z : Sym α n} (ha : a z) (hz : z List.sym n xs) :
a xs
theorem List.first_mem_of_cons_mem_sym {α : Type u_1} {xs : List α} {n : } {a : α} {z : Sym α n} (h : a ::ₛ z List.sym (n + 1) xs) :
a xs
theorem List.Nodup.sym {α : Type u_1} (n : ) {xs : List α} (h : ) :
theorem List.length_sym {α : Type u_1} {n : } {xs : List α} :