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

source
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

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

Instances For

source
theorem List.sym2_map {α : Type u_1} {β : Type u_2} (f : α → β) (xs : List α) :
(map f xs).sym2 = map (Sym2.map f) xs.sym2
source
theorem List.mem_sym2_cons_iff {α : Type u_1} {x : α} {xs : List α} {z : Sym2 α} :
z ∈ (x :: xs).sym2 ↔ z = s(x, x) ∨ (∃ y ∈ xs, z = s(x, y)) ∨ z ∈ xs.sym2
source
@[simp]
theorem List.sym2_eq_nil_iff {α : Type u_1} {xs : List α} :
xs.sym2 = [] ↔ xs = []
source
theorem List.left_mem_of_mk_mem_sym2 {α : Type u_1} {xs : List α} {a b : α} (h : s(a, b) ∈ xs.sym2) :
a ∈ xs
source
theorem List.right_mem_of_mk_mem_sym2 {α : Type u_1} {xs : List α} {a b : α} (h : s(a, b) ∈ xs.sym2) :
b ∈ xs
source
theorem List.mk_mem_sym2 {α : Type u_1} {xs : List α} {a b : α} (ha : a ∈ xs) (hb : b ∈ xs) :
s(a, b) ∈ xs.sym2
source
theorem List.mk_mem_sym2_iff {α : Type u_1} {xs : List α} {a b : α} :
s(a, b) ∈ xs.sym2 ↔ a ∈ xs ∧ b ∈ xs
source
theorem List.mem_sym2_iff {α : Type u_1} {xs : List α} {z : Sym2 α} :
z ∈ xs.sym2 ↔ ∀ y ∈ z, y ∈ xs
source
theorem List.setOf_mem_sym2 {α : Type u_1} {xs : List α} :
{z : Sym2 α | z ∈ xs.sym2} = {x : α | x ∈ xs}.sym2
source
theorem List.Nodup.sym2 {α : Type u_1} {xs : List α} (h : xs.Nodup) :
xs.sym2.Nodup
source
theorem List.map_mk_sublist_sym2 {α : Type u_1} (x : α) (xs : List α) (h : x ∈ xs) :
(map (fun (y : α) => s(x, y)) xs).Sublist xs.sym2
source
theorem List.map_mk_disjoint_sym2 {α : Type u_1} (x : α) (xs : List α) (h : x ∉ xs) :
(map (fun (y : α) => s(x, y)) xs).Disjoint xs.sym2
source
theorem List.dedup_sym2 {α : Type u_1} [DecidableEq α] (xs : List α) :
xs.sym2.dedup = xs.dedup.sym2
source
theorem List.Perm.sym2 {α : Type u_1} {xs ys : List α} (h : xs.Perm ys) :
xs.sym2.Perm ys.sym2
source
theorem List.Sublist.sym2 {α : Type u_1} {xs ys : List α} (h : xs.Sublist ys) :
xs.sym2.Sublist ys.sym2
source
theorem List.Subperm.sym2 {α : Type u_1} {xs ys : List α} (h : xs.Subperm ys) :
xs.sym2.Subperm ys.sym2
source
theorem List.length_sym2 {α : Type u_1} {xs : List α} :
xs.sym2.length = (xs.length + 1).choose 2
source
@[irreducible]
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 n.succ (x_2 :: xs) = List.map (fun (p : Sym α n) => x_2 ::ₛ p) (List.sym n (x_2 :: xs)) ++ List.sym (n + 1) xs

Instances For

source
theorem List.sym_one_eq {α : Type u_1} {xs : List α} :
List.sym 1 xs = map (fun (x : α) => x ::ₛ Sym.nil) xs
source
theorem List.sym2_eq_sym_two {α : Type u_1} {xs : List α} :
map (⇑(Sym2.equivSym α)) xs.sym2 = List.sym 2 xs
source
@[irreducible]
theorem List.sym_map {α : Type u_1} {β : Type u_3} (f : α → β) (n : ℕ) (xs : List α) :
List.sym n (map f xs) = map (Sym.map f) (List.sym n xs)
source
@[irreducible]
theorem List.Sublist.sym {α : Type u_1} (n : ℕ) {xs ys : List α} (h : xs.Sublist ys) :
(List.sym n xs).Sublist (List.sym n ys)
source
theorem List.sym_sublist_sym_cons {α : Type u_1} {xs : List α} {n : ℕ} {a : α} :
(List.sym n xs).Sublist (List.sym n (a :: xs))
source
@[irreducible]
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
source
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
source
@[irreducible]
theorem List.Nodup.sym {α : Type u_1} (n : ℕ) {xs : List α} (h : xs.Nodup) :
(List.sym n xs).Nodup
source
@[irreducible]
theorem List.length_sym {α : Type u_1} {n : ℕ} {xs : List α} :
(List.sym n xs).length = xs.length.multichoose n