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

• List.sym2 [] = []
• List.sym2 (x_1 :: xs) = List.map (fun (y : α) => s(x_1, y)) (x_1 :: xs) ++ List.sym2 xs

theorem List.mem_sym2_cons_iff {α : Type u_1} {x : α} {xs : List α} {z : Sym2 α} : z ∈ List.sym2 (x :: xs) ↔ z = s(x, x) ∨ (∃ y ∈ xs, z = s(x, y)) ∨ z ∈ List.sym2 xs

@[simp]

theorem List.sym2_eq_nil_iff {α : Type u_1} {xs : List α} : List.sym2 xs = [] ↔ xs = []

theorem List.left_mem_of_mk_mem_sym2 {α : Type u_1} {xs : List α} {a : α} {b : α} (h : s(a, b) ∈ List.sym2 xs) : a ∈ xs

theorem List.right_mem_of_mk_mem_sym2 {α : Type u_1} {xs : List α} {a : α} {b : α} (h : s(a, b) ∈ List.sym2 xs) : b ∈ xs

theorem List.mk_mem_sym2 {α : Type u_1} {xs : List α} {a : α} {b : α} (ha : a ∈ xs) (hb : b ∈ xs) : s(a, b) ∈ List.sym2 xs

theorem List.mk_mem_sym2_iff {α : Type u_1} {xs : List α} {a : α} {b : α} : s(a, b) ∈ List.sym2 xs ↔ a ∈ xs ∧ b ∈ xs

theorem List.mem_sym2_iff {α : Type u_1} {xs : List α} {z : Sym2 α} : z ∈ List.sym2 xs ↔ ∀ y ∈ z, y ∈ xs

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

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

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.Subperm.sym2 {α : Type u_1} {xs : List α} {ys : List α} (h : List.Subperm xs ys) : List.Subperm (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

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

• List.sym 0 x = [Sym.nil]
• List.sym x [] = []
• List.sym (Nat.succ n) (x_2 :: xs) = List.map (fun (p : Sym α n) => x_2 ::ₛ p) (List.sym n (x_2 :: xs)) ++ List.sym (n + 1) xs

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 (⇑(Sym2.equivSym α)) (List.sym2 xs) = 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 (Sym.map f) (List.sym n 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.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 : 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