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.instTransListPerm {α : Type u_3} : Trans List.Perm List.Perm List.Perm

Equations

• List.instTransListPerm = { trans := (_ : ∀ {l₁ l₂ l₃ : List α}, List.Perm l₁ l₂ → List.Perm l₂ l₃ → List.Perm l₁ l₃) }

theorem List.perm_rfl {α : Type u_1} {l : List α} : List.Perm l l

theorem List.Perm.subset_congr_left {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₃ : List α} (h : List.Perm l₁ l₂) : l₁ ⊆ l₃ ↔ l₂ ⊆ l₃

theorem List.Perm.subset_congr_right {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₃ : List α} (h : List.Perm l₁ 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 : List.Perm l 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} : Relation.Comp (List.Forall₂ r) List.Perm = Relation.Comp List.Perm (List.Forall₂ r)

theorem List.rel_perm_imp {α : Type u_1} {β : Type u_2} {r : α → β → Prop} (hr : Relator.RightUnique r) : (List.Forall₂ r ⇒ List.Forall₂ r ⇒ fun (x x_1 : Prop) => x → x_1) 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 (x x_1 : Prop) => x ↔ x_1) List.Perm List.Perm

theorem List.subperm_iff {α : Type u_1} {l₁ : List α} {l₂ : List α} : List.Subperm l₁ l₂ ↔ ∃ (l : List α), List.Perm l l₂ ∧ List.Sublist l₁ l

@[simp]

theorem List.subperm_singleton_iff {α : Type u_1} {l : List α} {a : α} : List.Subperm l [a] ↔ l = [] ∨ l = [a]

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 : List.Perm l₁ 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 : List.Perm l₁ l₂) (b : β) : List.foldr f b l₁ = List.foldr f b l₂

theorem List.Perm.fold_op_eq {α : Type u_1} {op : α → α → α} [IA : Std.Associative op] [IC : Std.Commutative op] {l₁ : List α} {l₂ : List α} {a : α} (h : List.Perm l₁ l₂) : List.foldl op a l₁ = List.foldl op a l₂

theorem List.Perm.sum_eq' {α : Type u_1} [M : AddMonoid α] {l₁ : List α} {l₂ : List α} (h : List.Perm l₁ l₂) (hc : List.Pairwise AddCommute l₁) : List.sum l₁ = List.sum l₂

If elements of a list additively commute with each other, then their sum does not depend on the order of elements.

theorem List.Perm.prod_eq' {α : Type u_1} [M : Monoid α] {l₁ : List α} {l₂ : List α} (h : List.Perm l₁ l₂) (hc : List.Pairwise Commute l₁) : List.prod l₁ = List.prod l₂

If elements of a list commute with each other, then their product does not depend on the order of elements.

theorem List.Perm.sum_eq {α : Type u_1} [AddCommMonoid α] {l₁ : List α} {l₂ : List α} (h : List.Perm l₁ l₂) : List.sum l₁ = List.sum l₂

theorem List.Perm.prod_eq {α : Type u_1} [CommMonoid α] {l₁ : List α} {l₂ : List α} (h : List.Perm l₁ l₂) : List.prod l₁ = List.prod l₂

theorem List.sum_reverse {α : Type u_1} [AddCommMonoid α] (l : List α) : List.sum (List.reverse l) = List.sum l

theorem List.prod_reverse {α : Type u_1} [CommMonoid α] (l : List α) : List.prod (List.reverse l) = List.prod l

theorem List.perm_option_to_list {α : Type u_1} {o₁ : Option α} {o₂ : Option α} : List.Perm (Option.toList o₁) (Option.toList o₂) ↔ o₁ = o₂

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

Alias of the reverse direction of List.subperm_cons.

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

Alias of the forward direction of List.subperm_cons.

theorem List.cons_subperm_of_mem {α : Type u_1} {a : α} {l₁ : List α} {l₂ : List α} (d₁ : List.Nodup l₁) (h₁ : a ∉ l₁) (h₂ : a ∈ l₂) (s : List.Subperm l₁ l₂) : List.Subperm (a :: l₁) l₂

theorem List.Nodup.subperm {α : Type u_1} {l₁ : List α} {l₂ : List α} (d : List.Nodup l₁) (H : l₁ ⊆ l₂) : List.Subperm l₁ l₂

theorem List.Perm.bagInter_right {α : Type u_1} [DecidableEq α] {l₁ : List α} {l₂ : List α} (t : List α) (h : List.Perm l₁ l₂) : List.Perm (List.bagInter l₁ t) (List.bagInter l₂ t)

theorem List.Perm.bagInter_left {α : Type u_1} [DecidableEq α] (l : List α) {t₁ : List α} {t₂ : List α} (p : List.Perm t₁ t₂) : List.bagInter l t₁ = List.bagInter l t₂

theorem List.Perm.bagInter {α : Type u_1} [DecidableEq α] {l₁ : List α} {l₂ : List α} {t₁ : List α} {t₂ : List α} (hl : List.Perm l₁ l₂) (ht : List.Perm t₁ t₂) : List.Perm (List.bagInter l₁ t₁) (List.bagInter l₂ t₂)

theorem List.perm_replicate_append_replicate {α : Type u_1} [DecidableEq α] {l : List α} {a : α} {b : α} {m : ℕ} {n : ℕ} (h : a ≠ b) : List.Perm l (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 : List.Perm l₁ l₂) : List.Perm (List.dedup l₁) (List.dedup l₂)

theorem List.Perm.inter_append {α : Type u_1} [DecidableEq α] {l : List α} {t₁ : List α} {t₂ : List α} (h : List.Disjoint t₁ t₂) : List.Perm (l ∩ (t₁ ++ t₂)) (l ∩ t₁ ++ l ∩ t₂)

theorem List.Perm.bind_left {α : Type u_1} {β : Type u_2} (l : List α) {f : α → List β} {g : α → List β} (h : ∀ a ∈ l, List.Perm (f a) (g a)) : List.Perm (List.bind l f) (List.bind l g)

theorem List.bind_append_perm {α : Type u_1} {β : Type u_2} (l : List α) (f : α → List β) (g : α → List β) : List.Perm (List.bind l f ++ List.bind l g) (List.bind l fun (x : α) => f x ++ g x)

theorem List.map_append_bind_perm {α : Type u_1} {β : Type u_2} (l : List α) (f : α → β) (g : α → List β) : List.Perm (List.map f l ++ List.bind l g) (List.bind l fun (x : α) => f x :: g x)

theorem List.Perm.product_right {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List α} (t₁ : List β) (p : List.Perm l₁ l₂) : List.Perm (List.product l₁ t₁) (List.product l₂ t₁)

theorem List.Perm.product_left {α : Type u_1} {β : Type u_2} (l : List α) {t₁ : List β} {t₂ : List β} (p : List.Perm t₁ t₂) : List.Perm (List.product l t₁) (List.product l t₂)

theorem List.Perm.product {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List α} {t₁ : List β} {t₂ : List β} (p₁ : List.Perm l₁ l₂) (p₂ : List.Perm t₁ t₂) : List.Perm (List.product l₁ t₁) (List.product l₂ t₂)

theorem List.perm_lookmap {α : Type u_1} (f : α → Option α) {l₁ : List α} {l₂ : List α} (H : List.Pairwise (fun (a b : α) => ∀ c ∈ f a, ∀ d ∈ f b, a = b ∧ c = d) l₁) (p : List.Perm l₁ l₂) : List.Perm (List.lookmap f l₁) (List.lookmap f l₂)

@[deprecated List.Perm.eraseP]

theorem List.Perm.erasep {α : Type u_1} (f : α → Prop) [DecidablePred f] {l₁ : List α} {l₂ : List α} (H : List.Pairwise (fun (a b : α) => f a → f b → False) l₁) (p : List.Perm l₁ l₂) : List.Perm (List.eraseP (fun (b : α) => decide (f b)) l₁) (List.eraseP (fun (b : α) => decide (f b)) l₂)

theorem List.Perm.take_inter {α : Type u_3} [DecidableEq α] {xs : List α} {ys : List α} (n : ℕ) (h : List.Perm xs ys) (h' : List.Nodup ys) : List.Perm (List.take n xs) (List.inter ys (List.take n xs))

theorem List.Perm.drop_inter {α : Type u_3} [DecidableEq α] {xs : List α} {ys : List α} (n : ℕ) (h : List.Perm xs ys) (h' : List.Nodup ys) : List.Perm (List.drop n xs) (List.inter ys (List.drop n xs))

theorem List.Perm.dropSlice_inter {α : Type u_3} [DecidableEq α] {xs : List α} {ys : List α} (n : ℕ) (m : ℕ) (h : List.Perm xs ys) (h' : List.Nodup ys) : List.Perm (List.dropSlice n m xs) (ys ∩ List.dropSlice n m xs)

theorem List.perm_of_mem_permutationsAux {α : Type u_1} {ts : List α} {is : List α} {l : List α} : l ∈ List.permutationsAux ts is → List.Perm l (ts ++ is)

theorem List.perm_of_mem_permutations {α : Type u_1} {l₁ : List α} {l₂ : List α} (h : l₁ ∈ List.permutations l₂) : List.Perm l₁ l₂

theorem List.length_permutationsAux {α : Type u_1} (ts : List α) (is : List α) : List.length (List.permutationsAux ts is) + Nat.factorial (List.length is) = Nat.factorial (List.length ts + List.length is)

theorem List.length_permutations {α : Type u_1} (l : List α) : List.length (List.permutations l) = Nat.factorial (List.length l)

theorem List.mem_permutations_of_perm_lemma {α : Type u_1} {is : List α} {l : List α} (H : List.Perm l ([] ++ is) → (∃ (ts' : List α) (_ : List.Perm ts' []), l = ts' ++ is) ∨ l ∈ List.permutationsAux is []) : List.Perm l is → l ∈ List.permutations is

theorem List.mem_permutationsAux_of_perm {α : Type u_1} {ts : List α} {is : List α} {l : List α} : List.Perm l (is ++ ts) → (∃ (is' : List α) (_ : List.Perm is' is), l = is' ++ ts) ∨ l ∈ List.permutationsAux ts is

@[simp]

theorem List.mem_permutations {α : Type u_1} {s : List α} {t : List α} : s ∈ List.permutations t ↔ List.Perm s t

theorem List.perm_permutations'Aux_comm {α : Type u_1} (a : α) (b : α) (l : List α) : List.Perm (List.bind (List.permutations'Aux a l) (List.permutations'Aux b)) (List.bind (List.permutations'Aux b l) (List.permutations'Aux a))

theorem List.Perm.permutations' {α : Type u_1} {s : List α} {t : List α} (p : List.Perm s t) : List.Perm (List.permutations' s) (List.permutations' t)

theorem List.permutations_perm_permutations' {α : Type u_1} (ts : List α) : List.Perm (List.permutations ts) (List.permutations' ts)

@[simp]

theorem List.mem_permutations' {α : Type u_1} {s : List α} {t : List α} : s ∈ List.permutations' t ↔ List.Perm s t

theorem List.Perm.permutations {α : Type u_1} {s : List α} {t : List α} (h : List.Perm s t) : List.Perm (List.permutations s) (List.permutations t)

@[simp]

theorem List.perm_permutations_iff {α : Type u_1} {s : List α} {t : List α} : List.Perm (List.permutations s) (List.permutations t) ↔ List.Perm s t

@[simp]

theorem List.perm_permutations'_iff {α : Type u_1} {s : List α} {t : List α} : List.Perm (List.permutations' s) (List.permutations' t) ↔ List.Perm s t

theorem List.nthLe_permutations'Aux {α : Type u_1} (s : List α) (x : α) (n : ℕ) (hn : n < List.length (List.permutations'Aux x s)) : List.nthLe (List.permutations'Aux x s) 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.length (List.takeWhile (fun (x_1 : α) => decide (x = x_1)) l) + 1

@[simp]

theorem List.length_permutations'Aux {α : Type u_1} (s : List α) (x : α) : List.length (List.permutations'Aux x s) = List.length s + 1

@[simp]

theorem List.permutations'Aux_nthLe_zero {α : Type u_1} (s : List α) (x : α) (hn : optParam (0 < List.length (List.permutations'Aux x s)) (_ : 0 < List.length (List.permutations'Aux x s))) : List.nthLe (List.permutations'Aux x s) 0 hn = x :: s

theorem List.injective_permutations'Aux {α : Type u_1} (x : α) : Function.Injective (List.permutations'Aux x)

theorem List.nodup_permutations'Aux_of_not_mem {α : Type u_1} (s : List α) (x : α) (hx : x ∉ s) : List.Nodup (List.permutations'Aux x s)

theorem List.nodup_permutations'Aux_iff {α : Type u_1} {s : List α} {x : α} : List.Nodup (List.permutations'Aux x s) ↔ x ∉ s

theorem List.nodup_permutations {α : Type u_1} (s : List α) (hs : List.Nodup s) : List.Nodup (List.permutations s)