Documentation

Mathlib.Data.List.Perm

List Permutations #

This file introduces the List.Perm relation, which is true if two lists are permutations of one another.

Notation #

The notation ~ is used for permutation equivalence.

instance List.instTransPerm_mathlib {α : Type u_1} :
Trans List.Perm List.Perm List.Perm
Equations
  • List.instTransPerm_mathlib = { trans := }
theorem List.perm_rfl {α : Type u_1} {l : List α} :
l.Perm l
theorem List.Perm.subset_congr_left {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₃ : List α} (h : l₁.Perm l₂) :
l₁ l₃ l₂ l₃
theorem List.Perm.subset_congr_right {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₃ : List α} (h : l₁.Perm l₂) :
l₃ l₁ l₃ l₂
theorem List.perm_comp_perm {α : Type u_1} :
Relation.Comp List.Perm List.Perm = List.Perm
theorem List.perm_comp_forall₂ {α : Type u_1} {β : Type u_2} {r : αβProp} {l : List α} {u : List α} {v : List β} (hlu : l.Perm u) (huv : List.Forall₂ r u v) :
Relation.Comp (List.Forall₂ r) List.Perm l v
theorem List.forall₂_comp_perm_eq_perm_comp_forall₂ {α : Type u_1} {β : Type u_2} {r : αβProp} :
theorem List.rel_perm_imp {α : Type u_1} {β : Type u_2} {r : αβProp} (hr : Relator.RightUnique r) :
(List.Forall₂ r List.Forall₂ r fun (x1 x2 : Prop) => x1x2) List.Perm List.Perm
theorem List.rel_perm {α : Type u_1} {β : Type u_2} {r : αβProp} (hr : Relator.BiUnique r) :
(List.Forall₂ r List.Forall₂ r fun (x1 x2 : Prop) => x1 x2) List.Perm List.Perm
theorem List.subperm_iff {α : Type u_1} {l₁ : List α} {l₂ : List α} :
l₁.Subperm l₂ ∃ (l : List α), l.Perm l₂ l₁.Sublist l
@[simp]
theorem List.subperm_singleton_iff {α : Type u_1} {l : List α} {a : α} :
l.Subperm [a] l = [] l = [a]
@[simp]
theorem List.subperm_nil {α : Type u_1} {l : List α} :
l.Subperm [] l = []
theorem List.subperm_cons_self {α : Type u_1} {l : List α} {a : α} :
l.Subperm (a :: l)
theorem List.count_eq_count_filter_add {α : Type u_1} [DecidableEq α] (P : αProp) [DecidablePred P] (l : List α) (a : α) :
List.count a l = List.count a (List.filter (fun (b : α) => decide (P b)) l) + List.count a (List.filter (fun (x : α) => decide ¬P x) l)
theorem List.Perm.foldl_eq {α : Type u_1} {β : Type u_2} {f : βαβ} {l₁ : List α} {l₂ : List α} [rcomm : RightCommutative f] (p : l₁.Perm l₂) (b : β) :
List.foldl f b l₁ = List.foldl f b l₂
theorem List.Perm.foldr_eq {α : Type u_1} {β : Type u_2} {f : αββ} {l₁ : List α} {l₂ : List α} [lcomm : LeftCommutative f] (p : l₁.Perm l₂) (b : β) :
List.foldr f b l₁ = List.foldr f b l₂
theorem List.Perm.foldl_op_eq {α : Type u_1} {op : ααα} [IA : Std.Associative op] [IC : Std.Commutative op] {l₁ : List α} {l₂ : List α} {a : α} (h : l₁.Perm l₂) :
List.foldl op a l₁ = List.foldl op a l₂
theorem List.Perm.foldr_op_eq {α : Type u_1} {op : ααα} [IA : Std.Associative op] [IC : Std.Commutative op] {l₁ : List α} {l₂ : List α} {a : α} (h : l₁.Perm l₂) :
List.foldr op a l₁ = List.foldr op a l₂
@[deprecated List.Perm.foldl_op_eq]
theorem List.Perm.fold_op_eq {α : Type u_1} {op : ααα} [IA : Std.Associative op] [IC : Std.Commutative op] {l₁ : List α} {l₂ : List α} {a : α} (h : l₁.Perm l₂) :
List.foldl op a l₁ = List.foldl op a l₂

Alias of List.Perm.foldl_op_eq.

theorem List.perm_option_to_list {α : Type u_1} {o₁ : Option α} {o₂ : Option α} :
o₁.toList.Perm o₂.toList o₁ = o₂
theorem List.subperm.of_cons {α : Type u_1} (a : α) {l₁ : List α} {l₂ : List α} :
(a :: l₁).Subperm (a :: l₂)l₁.Subperm l₂

Alias of the forward direction of List.subperm_cons.

theorem List.subperm.cons {α : Type u_1} (a : α) {l₁ : List α} {l₂ : List α} :
l₁.Subperm l₂(a :: l₁).Subperm (a :: l₂)

Alias of the reverse direction of List.subperm_cons.

theorem List.cons_subperm_of_mem {α : Type u_1} {a : α} {l₁ : List α} {l₂ : List α} (d₁ : l₁.Nodup) (h₁ : al₁) (h₂ : a l₂) (s : l₁.Subperm l₂) :
(a :: l₁).Subperm l₂
theorem List.Nodup.subperm {α : Type u_1} {l₁ : List α} {l₂ : List α} (d : l₁.Nodup) (H : l₁ l₂) :
l₁.Subperm l₂
theorem List.Perm.bagInter_right {α : Type u_1} [DecidableEq α] {l₁ : List α} {l₂ : List α} (t : List α) (h : l₁.Perm l₂) :
(l₁.bagInter t).Perm (l₂.bagInter t)
theorem List.Perm.bagInter_left {α : Type u_1} [DecidableEq α] (l : List α) {t₁ : List α} {t₂ : List α} (p : t₁.Perm t₂) :
l.bagInter t₁ = l.bagInter t₂
theorem List.Perm.bagInter {α : Type u_1} [DecidableEq α] {l₁ : List α} {l₂ : List α} {t₁ : List α} {t₂ : List α} (hl : l₁.Perm l₂) (ht : t₁.Perm t₂) :
(l₁.bagInter t₁).Perm (l₂.bagInter t₂)
theorem List.perm_replicate_append_replicate {α : Type u_1} [DecidableEq α] {l : List α} {a : α} {b : α} {m : } {n : } (h : a b) :
l.Perm (List.replicate m a ++ List.replicate n b) List.count a l = m List.count b l = n l [a, b]
theorem List.Perm.dedup {α : Type u_1} [DecidableEq α] {l₁ : List α} {l₂ : List α} (p : l₁.Perm l₂) :
l₁.dedup.Perm l₂.dedup
theorem List.Perm.inter_append {α : Type u_1} [DecidableEq α] {l : List α} {t₁ : List α} {t₂ : List α} (h : t₁.Disjoint t₂) :
(l (t₁ ++ t₂)).Perm (l t₁ ++ l t₂)
theorem List.Perm.bind_left {α : Type u_1} {β : Type u_2} (l : List α) {f : αList β} {g : αList β} (h : al, (f a).Perm (g a)) :
(l.bind f).Perm (l.bind g)
theorem List.bind_append_perm {α : Type u_1} {β : Type u_2} (l : List α) (f : αList β) (g : αList β) :
(l.bind f ++ l.bind g).Perm (l.bind fun (x : α) => f x ++ g x)
theorem List.map_append_bind_perm {α : Type u_1} {β : Type u_2} (l : List α) (f : αβ) (g : αList β) :
(List.map f l ++ l.bind g).Perm (l.bind fun (x : α) => f x :: g x)
theorem List.Perm.product_right {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List α} (t₁ : List β) (p : l₁.Perm l₂) :
(l₁.product t₁).Perm (l₂.product t₁)
theorem List.Perm.product_left {α : Type u_1} {β : Type u_2} (l : List α) {t₁ : List β} {t₂ : List β} (p : t₁.Perm t₂) :
(l.product t₁).Perm (l.product t₂)
theorem List.Perm.product {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List α} {t₁ : List β} {t₂ : List β} (p₁ : l₁.Perm l₂) (p₂ : t₁.Perm t₂) :
(l₁.product t₁).Perm (l₂.product t₂)
theorem List.perm_lookmap {α : Type u_1} (f : αOption α) {l₁ : List α} {l₂ : List α} (H : List.Pairwise (fun (a b : α) => cf a, df b, a = b c = d) l₁) (p : l₁.Perm l₂) :
(List.lookmap f l₁).Perm (List.lookmap f l₂)
theorem List.Perm.take_inter {α : Type u_1} [DecidableEq α] {xs : List α} {ys : List α} (n : ) (h : xs.Perm ys) (h' : ys.Nodup) :
(List.take n xs).Perm (ys.inter (List.take n xs))
theorem List.Perm.drop_inter {α : Type u_1} [DecidableEq α] {xs : List α} {ys : List α} (n : ) (h : xs.Perm ys) (h' : ys.Nodup) :
(List.drop n xs).Perm (ys.inter (List.drop n xs))
theorem List.Perm.dropSlice_inter {α : Type u_1} [DecidableEq α] {xs : List α} {ys : List α} (n : ) (m : ) (h : xs.Perm ys) (h' : ys.Nodup) :
(List.dropSlice n m xs).Perm (ys List.dropSlice n m xs)
theorem List.perm_of_mem_permutationsAux {α : Type u_1} {ts : List α} {is : List α} {l : List α} :
l ts.permutationsAux isl.Perm (ts ++ is)
theorem List.perm_of_mem_permutations {α : Type u_1} {l₁ : List α} {l₂ : List α} (h : l₁ l₂.permutations) :
l₁.Perm l₂
theorem List.length_permutationsAux {α : Type u_1} (ts : List α) (is : List α) :
(ts.permutationsAux is).length + is.length.factorial = (ts.length + is.length).factorial
theorem List.length_permutations {α : Type u_1} (l : List α) :
l.permutations.length = l.length.factorial
theorem List.mem_permutations_of_perm_lemma {α : Type u_1} {is : List α} {l : List α} (H : l.Perm ([] ++ is)(∃ (ts' : List α) (_ : ts'.Perm []), l = ts' ++ is) l is.permutationsAux []) :
l.Perm isl is.permutations
theorem List.mem_permutationsAux_of_perm {α : Type u_1} {ts : List α} {is : List α} {l : List α} :
l.Perm (is ++ ts)(∃ (is' : List α) (_ : is'.Perm is), l = is' ++ ts) l ts.permutationsAux is
@[simp]
theorem List.mem_permutations {α : Type u_1} {s : List α} {t : List α} :
s t.permutations s.Perm t
theorem List.perm_permutations'Aux_comm {α : Type u_1} (a : α) (b : α) (l : List α) :
theorem List.Perm.permutations' {α : Type u_1} {s : List α} {t : List α} (p : s.Perm t) :
s.permutations'.Perm t.permutations'
theorem List.permutations_perm_permutations' {α : Type u_1} (ts : List α) :
ts.permutations.Perm ts.permutations'
@[simp]
theorem List.mem_permutations' {α : Type u_1} {s : List α} {t : List α} :
s t.permutations' s.Perm t
theorem List.Perm.permutations {α : Type u_1} {s : List α} {t : List α} (h : s.Perm t) :
s.permutations.Perm t.permutations
@[simp]
theorem List.perm_permutations_iff {α : Type u_1} {s : List α} {t : List α} :
s.permutations.Perm t.permutations s.Perm t
@[simp]
theorem List.perm_permutations'_iff {α : Type u_1} {s : List α} {t : List α} :
s.permutations'.Perm t.permutations' s.Perm t
theorem List.getElem_permutations'Aux {α : Type u_1} (s : List α) (x : α) (n : ) (hn : n < (List.permutations'Aux x s).length) :
theorem List.get_permutations'Aux {α : Type u_1} (s : List α) (x : α) (n : ) (hn : n < (List.permutations'Aux x s).length) :
(List.permutations'Aux x s).get n, hn = List.insertNth n x s
theorem List.count_permutations'Aux_self {α : Type u_1} [DecidableEq α] (l : List α) (x : α) :
List.count (x :: l) (List.permutations'Aux x l) = (List.takeWhile (fun (x_1 : α) => decide (x = x_1)) l).length + 1
@[simp]
theorem List.length_permutations'Aux {α : Type u_1} (s : List α) (x : α) :
(List.permutations'Aux x s).length = s.length + 1
@[deprecated]
theorem List.permutations'Aux_get_zero {α : Type u_1} (s : List α) (x : α) (hn : optParam (0 < (List.permutations'Aux x s).length) ) :
(List.permutations'Aux x s).get 0, hn = x :: s
theorem List.nodup_permutations'Aux_of_not_mem {α : Type u_1} (s : List α) (x : α) (hx : xs) :
theorem List.nodup_permutations'Aux_iff {α : Type u_1} {s : List α} {x : α} :
(List.permutations'Aux x s).Nodup xs
theorem List.nodup_permutations {α : Type u_1} (s : List α) (hs : s.Nodup) :
s.permutations.Nodup
theorem List.permutations_take_two {α : Type u_1} (x : α) (y : α) (s : List α) :
List.take 2 (x :: y :: s).permutations = [x :: y :: s, y :: x :: s]
@[simp]
theorem List.nodup_permutations_iff {α : Type u_1} {s : List α} :
s.permutations.Nodup s.Nodup