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 #

TODO #

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
    theorem List.sym2_map {α : Type u_1} {β : Type u_2} (f : αβ) (xs : List α) :
    (List.map f xs).sym2 = List.map (Sym2.map f) xs.sym2
    theorem List.mem_sym2_cons_iff {α : Type u_1} {x : α} {xs : List α} {z : Sym2 α} :
    z (x :: xs).sym2 z = s(x, x) (∃ yxs, z = s(x, y)) z xs.sym2
    @[simp]
    theorem List.sym2_eq_nil_iff {α : Type u_1} {xs : List α} :
    xs.sym2 = [] xs = []
    theorem List.left_mem_of_mk_mem_sym2 {α : Type u_1} {xs : List α} {a : α} {b : α} (h : s(a, b) xs.sym2) :
    a xs
    theorem List.right_mem_of_mk_mem_sym2 {α : Type u_1} {xs : List α} {a : α} {b : α} (h : s(a, b) xs.sym2) :
    b xs
    theorem List.mk_mem_sym2 {α : Type u_1} {xs : List α} {a : α} {b : α} (ha : a xs) (hb : b xs) :
    s(a, b) xs.sym2
    theorem List.mk_mem_sym2_iff {α : Type u_1} {xs : List α} {a : α} {b : α} :
    s(a, b) xs.sym2 a xs b xs
    theorem List.mem_sym2_iff {α : Type u_1} {xs : List α} {z : Sym2 α} :
    z xs.sym2 yz, y xs
    theorem List.Nodup.sym2 {α : Type u_1} {xs : List α} (h : xs.Nodup) :
    xs.sym2.Nodup
    theorem List.map_mk_sublist_sym2 {α : Type u_1} (x : α) (xs : List α) (h : x xs) :
    (List.map (fun (y : α) => s(x, y)) xs).Sublist xs.sym2
    theorem List.map_mk_disjoint_sym2 {α : Type u_1} (x : α) (xs : List α) (h : xxs) :
    (List.map (fun (y : α) => s(x, y)) xs).Disjoint xs.sym2
    theorem List.dedup_sym2 {α : Type u_1} [DecidableEq α] (xs : List α) :
    xs.sym2.dedup = xs.dedup.sym2
    theorem List.Perm.sym2 {α : Type u_1} {xs : List α} {ys : List α} (h : xs.Perm ys) :
    xs.sym2.Perm ys.sym2
    theorem List.Sublist.sym2 {α : Type u_1} {xs : List α} {ys : List α} (h : xs.Sublist ys) :
    xs.sym2.Sublist ys.sym2
    theorem List.Subperm.sym2 {α : Type u_1} {xs : List α} {ys : List α} (h : xs.Subperm ys) :
    xs.sym2.Subperm ys.sym2
    theorem List.length_sym2 {α : Type u_1} {xs : List α} :
    xs.sym2.length = (xs.length + 1).choose 2
    @[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
    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 (⇑(Sym2.equivSym α)) xs.sym2 = List.sym 2 xs
      @[irreducible]
      theorem List.sym_map {α : Type u_1} {β : Type u_3} (f : αβ) (n : ) (xs : List α) :
      @[irreducible]
      theorem List.Sublist.sym {α : Type u_1} (n : ) {xs : List α} {ys : List α} (h : xs.Sublist ys) :
      (List.sym n xs).Sublist (List.sym n ys)
      theorem List.sym_sublist_sym_cons {α : Type u_1} {xs : List α} {n : } {a : α} :
      (List.sym n xs).Sublist (List.sym n (a :: xs))
      @[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
      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
      @[irreducible]
      theorem List.Nodup.sym {α : Type u_1} (n : ) {xs : List α} (h : xs.Nodup) :
      (List.sym n xs).Nodup
      @[irreducible]
      theorem List.length_sym {α : Type u_1} {n : } {xs : List α} :
      (List.sym n xs).length = xs.length.multichoose n