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.

inductive list.perm {α : Type uu} :
list αlist α → Prop
• nil : ∀ {α : Type uu},
• cons : ∀ {α : Type uu} (x : α) {l₁ l₂ : list α}, l₁ ~ l₂x :: l₁ ~ x :: l₂
• swap : ∀ {α : Type uu} (x y : α) (l : list α), y :: x :: l ~ x :: y :: l
• trans : ∀ {α : Type uu} {l₁ l₂ l₃ : list α}, l₁ ~ l₂l₂ ~ l₃l₁ ~ l₃

perm l₁ l₂ or l₁ ~ l₂ asserts that l₁ and l₂ are permutations of each other. This is defined by induction using pairwise swaps.

Instances for list.perm
@[protected, refl]
theorem list.perm.refl {α : Type uu} (l : list α) :
l ~ l
@[protected, symm]
theorem list.perm.symm {α : Type uu} {l₁ l₂ : list α} (p : l₁ ~ l₂) :
l₂ ~ l₁
theorem list.perm_comm {α : Type uu} {l₁ l₂ : list α} :
l₁ ~ l₂ l₂ ~ l₁
theorem list.perm.swap' {α : Type uu} (x y : α) {l₁ l₂ : list α} (p : l₁ ~ l₂) :
y :: x :: l₁ ~ x :: y :: l₂
theorem list.perm.eqv (α : Type u_1) :
@[protected, instance]
def list.is_setoid (α : Type u_1) :
Equations
theorem list.perm.subset {α : Type uu} {l₁ l₂ : list α} (p : l₁ ~ l₂) :
l₁ l₂
theorem list.perm.mem_iff {α : Type uu} {a : α} {l₁ l₂ : list α} (h : l₁ ~ l₂) :
a l₁ a l₂
theorem list.perm.append_right {α : Type uu} {l₁ l₂ : list α} (t₁ : list α) (p : l₁ ~ l₂) :
l₁ ++ t₁ ~ l₂ ++ t₁
theorem list.perm.append_left {α : Type uu} {t₁ t₂ : list α} (l : list α) :
t₁ ~ t₂l ++ t₁ ~ l ++ t₂
theorem list.perm.append {α : Type uu} {l₁ l₂ t₁ t₂ : list α} (p₁ : l₁ ~ l₂) (p₂ : t₁ ~ t₂) :
l₁ ++ t₁ ~ l₂ ++ t₂
theorem list.perm.append_cons {α : Type uu} (a : α) {h₁ h₂ t₁ t₂ : list α} (p₁ : h₁ ~ h₂) (p₂ : t₁ ~ t₂) :
h₁ ++ a :: t₁ ~ h₂ ++ a :: t₂
@[simp]
theorem list.perm_middle {α : Type uu} {a : α} {l₁ l₂ : list α} :
l₁ ++ a :: l₂ ~ a :: (l₁ ++ l₂)
@[simp]
theorem list.perm_append_singleton {α : Type uu} (a : α) (l : list α) :
l ++ [a] ~ a :: l
theorem list.perm_append_comm {α : Type uu} {l₁ l₂ : list α} :
l₁ ++ l₂ ~ l₂ ++ l₁
theorem list.concat_perm {α : Type uu} (l : list α) (a : α) :
l.concat a ~ a :: l
theorem list.perm.length_eq {α : Type uu} {l₁ l₂ : list α} (p : l₁ ~ l₂) :
l₁.length = l₂.length
theorem list.perm.eq_nil {α : Type uu} {l : list α} (p : l ~ list.nil) :
theorem list.perm.nil_eq {α : Type uu} {l : list α} (p : list.nil ~ l) :
@[simp]
theorem list.perm_nil {α : Type uu} {l₁ : list α} :
@[simp]
theorem list.nil_perm {α : Type uu} {l₁ : list α} :
theorem list.not_perm_nil_cons {α : Type uu} (x : α) (l : list α) :
@[simp]
theorem list.reverse_perm {α : Type uu} (l : list α) :
theorem list.perm_cons_append_cons {α : Type uu} {l l₁ l₂ : list α} (a : α) (p : l ~ l₁ ++ l₂) :
a :: l ~ l₁ ++ a :: l₂
@[simp]
theorem list.perm_repeat {α : Type uu} {a : α} {n : } {l : list α} :
l ~ n l = n
@[simp]
theorem list.repeat_perm {α : Type uu} {a : α} {n : } {l : list α} :
n ~ l n = l
@[simp]
theorem list.perm_singleton {α : Type uu} {a : α} {l : list α} :
l ~ [a] l = [a]
@[simp]
theorem list.singleton_perm {α : Type uu} {a : α} {l : list α} :
[a] ~ l [a] = l
theorem list.perm.eq_singleton {α : Type uu} {a : α} {l : list α} (p : l ~ [a]) :
l = [a]
theorem list.perm.singleton_eq {α : Type uu} {a : α} {l : list α} (p : [a] ~ l) :
[a] = l
theorem list.singleton_perm_singleton {α : Type uu} {a b : α} :
[a] ~ [b] a = b
theorem list.perm_cons_erase {α : Type uu} [decidable_eq α] {a : α} {l : list α} (h : a l) :
l ~ a :: l.erase a
theorem list.perm_induction_on {α : Type uu} {P : list αlist α → Prop} {l₁ l₂ : list α} (p : l₁ ~ l₂) (h₁ : list.nil) (h₂ : ∀ (x : α) (l₁ l₂ : list α), l₁ ~ l₂P l₁ l₂P (x :: l₁) (x :: l₂)) (h₃ : ∀ (x y : α) (l₁ l₂ : list α), l₁ ~ l₂P l₁ l₂P (y :: x :: l₁) (x :: y :: l₂)) (h₄ : ∀ (l₁ l₂ l₃ : list α), l₁ ~ l₂l₂ ~ l₃P l₁ l₂P l₂ l₃P l₁ l₃) :
P l₁ l₂
theorem list.perm.filter_map {α : Type uu} {β : Type vv} (f : α → ) {l₁ l₂ : list α} (p : l₁ ~ l₂) :
l₁ ~ l₂
theorem list.perm.map {α : Type uu} {β : Type vv} (f : α → β) {l₁ l₂ : list α} (p : l₁ ~ l₂) :
l₁ ~ l₂
theorem list.perm.pmap {α : Type uu} {β : Type vv} {p : α → Prop} (f : Π (a : α), p a → β) {l₁ l₂ : list α} (p_1 : l₁ ~ l₂) {H₁ : ∀ (a : α), a l₁p a} {H₂ : ∀ (a : α), a l₂p a} :
l₁ H₁ ~ l₂ H₂
theorem list.perm.filter {α : Type uu} (p : α → Prop) {l₁ l₂ : list α} (s : l₁ ~ l₂) :
l₁ ~ l₂
theorem list.filter_append_perm {α : Type uu} (p : α → Prop) (l : list α) :
l ++ list.filter (λ (x : α), ¬p x) l ~ l
theorem list.exists_perm_sublist {α : Type uu} {l₁ l₂ l₂' : list α} (s : l₁ <+ l₂) (p : l₂ ~ l₂') :
∃ (l₁' : list α) (H : l₁' ~ l₁), l₁' <+ l₂'
theorem list.perm.sizeof_eq_sizeof {α : Type uu} [has_sizeof α] {l₁ l₂ : list α} (h : l₁ ~ l₂) :
l₁.sizeof = l₂.sizeof
theorem list.perm_comp_perm {α : Type uu} :
theorem list.perm_comp_forall₂ {α : Type uu} {β : Type vv} {r : α → β → Prop} {l u : list α} {v : list β} (hlu : l ~ u) (huv : u v) :
v
theorem list.forall₂_comp_perm_eq_perm_comp_forall₂ {α : Type uu} {β : Type vv} {r : α → β → Prop} :
theorem list.rel_perm_imp {α : Type uu} {β : Type vv} {r : α → β → Prop} (hr : relator.right_unique r) :
theorem list.rel_perm {α : Type uu} {β : Type vv} {r : α → β → Prop} (hr : relator.bi_unique r) :
def list.subperm {α : Type uu} (l₁ l₂ : list α) :
Prop

subperm l₁ l₂, denoted l₁ <+~ l₂, means that l₁ is a sublist of a permutation of l₂. This is an analogue of l₁ ⊆ l₂ which respects multiplicities of elements, and is used for the ≤ relation on multisets.

Equations
• l₁ <+~ l₂ = ∃ (l : list α) (H : l ~ l₁), l <+ l₂
theorem list.nil_subperm {α : Type uu} {l : list α} :
theorem list.perm.subperm_left {α : Type uu} {l l₁ l₂ : list α} (p : l₁ ~ l₂) :
l <+~ l₁ l <+~ l₂
theorem list.perm.subperm_right {α : Type uu} {l₁ l₂ l : list α} (p : l₁ ~ l₂) :
l₁ <+~ l l₂ <+~ l
theorem list.sublist.subperm {α : Type uu} {l₁ l₂ : list α} (s : l₁ <+ l₂) :
l₁ <+~ l₂
theorem list.perm.subperm {α : Type uu} {l₁ l₂ : list α} (p : l₁ ~ l₂) :
l₁ <+~ l₂
@[refl]
theorem list.subperm.refl {α : Type uu} (l : list α) :
l <+~ l
@[trans]
theorem list.subperm.trans {α : Type uu} {l₁ l₂ l₃ : list α} :
l₁ <+~ l₂l₂ <+~ l₃l₁ <+~ l₃
theorem list.subperm.length_le {α : Type uu} {l₁ l₂ : list α} :
l₁ <+~ l₂l₁.length l₂.length
theorem list.subperm.perm_of_length_le {α : Type uu} {l₁ l₂ : list α} :
l₁ <+~ l₂l₂.length l₁.lengthl₁ ~ l₂
theorem list.subperm.antisymm {α : Type uu} {l₁ l₂ : list α} (h₁ : l₁ <+~ l₂) (h₂ : l₂ <+~ l₁) :
l₁ ~ l₂
theorem list.subperm.subset {α : Type uu} {l₁ l₂ : list α} :
l₁ <+~ l₂l₁ l₂
theorem list.subperm.filter {α : Type uu} (p : α → Prop) ⦃l l' : list α⦄ (h : l <+~ l') :
l <+~ l'
theorem list.sublist.exists_perm_append {α : Type uu} {l₁ l₂ : list α} :
l₁ <+ l₂(∃ (l : list α), l₂ ~ l₁ ++ l)
theorem list.perm.countp_eq {α : Type uu} (p : α → Prop) {l₁ l₂ : list α} (s : l₁ ~ l₂) :
l₁ = l₂
theorem list.subperm.countp_le {α : Type uu} (p : α → Prop) {l₁ l₂ : list α} :
l₁ <+~ l₂ l₁ l₂
theorem list.perm.countp_congr {α : Type uu} {l₁ l₂ : list α} (s : l₁ ~ l₂) {p p' : α → Prop} [decidable_pred p'] (hp : ∀ (x : α), x l₁p x = p' x) :
l₁ = l₂
theorem list.countp_eq_countp_filter_add {α : Type uu} (l : list α) (p q : α → Prop)  :
l = l) + (list.filter (λ (a : α), ¬q a) l)
theorem list.perm.count_eq {α : Type uu} [decidable_eq α] {l₁ l₂ : list α} (p : l₁ ~ l₂) (a : α) :
l₁ = l₂
theorem list.subperm.count_le {α : Type uu} [decidable_eq α] {l₁ l₂ : list α} (s : l₁ <+~ l₂) (a : α) :
l₁ l₂
theorem list.perm.foldl_eq' {α : Type uu} {β : Type vv} {f : β → α → β} {l₁ l₂ : list α} (p : l₁ ~ l₂) :
(∀ (x : α), x l₁∀ (y : α), y l₁∀ (z : β), f (f z x) y = f (f z y) x)∀ (b : β), b l₁ = b l₂
theorem list.perm.foldl_eq {α : Type uu} {β : Type vv} {f : β → α → β} {l₁ l₂ : list α} (rcomm : right_commutative f) (p : l₁ ~ l₂) (b : β) :
b l₁ = b l₂
theorem list.perm.foldr_eq {α : Type uu} {β : Type vv} {f : α → β → β} {l₁ l₂ : list α} (lcomm : left_commutative f) (p : l₁ ~ l₂) (b : β) :
b l₁ = b l₂
theorem list.perm.rec_heq {α : Type uu} {β : list αSort u_1} {f : Π (a : α) (l : list α), β lβ (a :: l)} {b : β list.nil} {l l' : list α} (hl : l ~ l') (f_congr : ∀ {a : α} {l l' : list α} {b : β l} {b' : β l'}, l ~ l'b == b'f a l b == f a l' b') (f_swap : ∀ {a a' : α} {l : list α} {b : β l}, f a (a' :: l) (f a' l b) == f a' (a :: l) (f a l b)) :
list.rec b f l == list.rec b f l'
theorem list.perm.fold_op_eq {α : Type uu} {op : α → α → α} [ op] [ op] {l₁ l₂ : list α} {a : α} (h : l₁ ~ l₂) :
a l₁ = a l₂
theorem list.perm.prod_eq' {α : Type uu} [monoid α] {l₁ l₂ : list α} (h : l₁ ~ l₂) (hc : list.pairwise (λ (x y : α), x * y = y * x) l₁) :
l₁.prod = l₂.prod

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 uu} [add_monoid α] {l₁ l₂ : list α} (h : l₁ ~ l₂) (hc : list.pairwise (λ (x y : α), x + y = y + x) l₁) :
l₁.sum = l₂.sum
theorem list.perm.prod_eq {α : Type uu} [comm_monoid α] {l₁ l₂ : list α} (h : l₁ ~ l₂) :
l₁.prod = l₂.prod
theorem list.perm.sum_eq {α : Type uu} {l₁ l₂ : list α} (h : l₁ ~ l₂) :
l₁.sum = l₂.sum
theorem list.sum_reverse {α : Type uu} (l : list α) :
theorem list.prod_reverse {α : Type uu} [comm_monoid α] (l : list α) :
theorem list.perm_inv_core {α : Type uu} {a : α} {l₁ l₂ r₁ r₂ : list α} :
l₁ ++ a :: r₁ ~ l₂ ++ a :: r₂l₁ ++ r₁ ~ l₂ ++ r₂
theorem list.perm.cons_inv {α : Type uu} {a : α} {l₁ l₂ : list α} :
a :: l₁ ~ a :: l₂l₁ ~ l₂
@[simp]
theorem list.perm_cons {α : Type uu} (a : α) {l₁ l₂ : list α} :
a :: l₁ ~ a :: l₂ l₁ ~ l₂
theorem list.perm_append_left_iff {α : Type uu} {l₁ l₂ : list α} (l : list α) :
l ++ l₁ ~ l ++ l₂ l₁ ~ l₂
theorem list.perm_append_right_iff {α : Type uu} {l₁ l₂ : list α} (l : list α) :
l₁ ++ l ~ l₂ ++ l l₁ ~ l₂
theorem list.perm_option_to_list {α : Type uu} {o₁ o₂ : option α} :
o₁.to_list ~ o₂.to_list o₁ = o₂
theorem list.subperm_cons {α : Type uu} (a : α) {l₁ l₂ : list α} :
a :: l₁ <+~ a :: l₂ l₁ <+~ l₂
theorem list.subperm.of_cons {α : Type uu} (a : α) {l₁ l₂ : list α} :
a :: l₁ <+~ a :: l₂l₁ <+~ l₂

Alias of the forward direction of list.subperm_cons.

@[protected]
theorem list.subperm.cons {α : Type uu} (a : α) {l₁ l₂ : list α} :
l₁ <+~ l₂a :: l₁ <+~ a :: l₂

Alias of the reverse direction of list.subperm_cons.

theorem list.cons_subperm_of_mem {α : Type uu} {a : α} {l₁ l₂ : list α} (d₁ : l₁.nodup) (h₁ : a l₁) (h₂ : a l₂) (s : l₁ <+~ l₂) :
a :: l₁ <+~ l₂
theorem list.subperm_append_left {α : Type uu} {l₁ l₂ : list α} (l : list α) :
l ++ l₁ <+~ l ++ l₂ l₁ <+~ l₂
theorem list.subperm_append_right {α : Type uu} {l₁ l₂ : list α} (l : list α) :
l₁ ++ l <+~ l₂ ++ l l₁ <+~ l₂
theorem list.subperm.exists_of_length_lt {α : Type uu} {l₁ l₂ : list α} :
l₁ <+~ l₂l₁.length < l₂.length(∃ (a : α), a :: l₁ <+~ l₂)
@[protected]
theorem list.nodup.subperm {α : Type uu} {l₁ l₂ : list α} (d : l₁.nodup) (H : l₁ l₂) :
l₁ <+~ l₂
theorem list.perm_ext {α : Type uu} {l₁ l₂ : list α} (d₁ : l₁.nodup) (d₂ : l₂.nodup) :
l₁ ~ l₂ ∀ (a : α), a l₁ a l₂
theorem list.nodup.sublist_ext {α : Type uu} {l₁ l₂ l : list α} (d : l.nodup) (s₁ : l₁ <+ l) (s₂ : l₂ <+ l) :
l₁ ~ l₂ l₁ = l₂
theorem list.perm.erase {α : Type uu} [decidable_eq α] (a : α) {l₁ l₂ : list α} (p : l₁ ~ l₂) :
l₁.erase a ~ l₂.erase a
theorem list.subperm_cons_erase {α : Type uu} [decidable_eq α] (a : α) (l : list α) :
l <+~ a :: l.erase a
theorem list.erase_subperm {α : Type uu} [decidable_eq α] (a : α) (l : list α) :
l.erase a <+~ l
theorem list.subperm.erase {α : Type uu} [decidable_eq α] {l₁ l₂ : list α} (a : α) (h : l₁ <+~ l₂) :
l₁.erase a <+~ l₂.erase a
theorem list.perm.diff_right {α : Type uu} [decidable_eq α] {l₁ l₂ : list α} (t : list α) (h : l₁ ~ l₂) :
l₁.diff t ~ l₂.diff t
theorem list.perm.diff_left {α : Type uu} [decidable_eq α] (l : list α) {t₁ t₂ : list α} (h : t₁ ~ t₂) :
l.diff t₁ = l.diff t₂
theorem list.perm.diff {α : Type uu} [decidable_eq α] {l₁ l₂ t₁ t₂ : list α} (hl : l₁ ~ l₂) (ht : t₁ ~ t₂) :
l₁.diff t₁ ~ l₂.diff t₂
theorem list.subperm.diff_right {α : Type uu} [decidable_eq α] {l₁ l₂ : list α} (h : l₁ <+~ l₂) (t : list α) :
l₁.diff t <+~ l₂.diff t
theorem list.erase_cons_subperm_cons_erase {α : Type uu} [decidable_eq α] (a b : α) (l : list α) :
(a :: l).erase b <+~ a :: l.erase b
theorem list.subperm_cons_diff {α : Type uu} [decidable_eq α] {a : α} {l₁ l₂ : list α} :
(a :: l₁).diff l₂ <+~ a :: l₁.diff l₂
theorem list.subset_cons_diff {α : Type uu} [decidable_eq α] {a : α} {l₁ l₂ : list α} :
(a :: l₁).diff l₂ a :: l₁.diff l₂
theorem list.perm.bag_inter_right {α : Type uu} [decidable_eq α] {l₁ l₂ : list α} (t : list α) (h : l₁ ~ l₂) :
l₁.bag_inter t ~ l₂.bag_inter t
theorem list.perm.bag_inter_left {α : Type uu} [decidable_eq α] (l : list α) {t₁ t₂ : list α} (p : t₁ ~ t₂) :
l.bag_inter t₁ = l.bag_inter t₂
theorem list.perm.bag_inter {α : Type uu} [decidable_eq α] {l₁ l₂ t₁ t₂ : list α} (hl : l₁ ~ l₂) (ht : t₁ ~ t₂) :
l₁.bag_inter t₁ ~ l₂.bag_inter t₂
theorem list.cons_perm_iff_perm_erase {α : Type uu} [decidable_eq α] {a : α} {l₁ l₂ : list α} :
a :: l₁ ~ l₂ a l₂ l₁ ~ l₂.erase a
theorem list.perm_iff_count {α : Type uu} [decidable_eq α] {l₁ l₂ : list α} :
l₁ ~ l₂ ∀ (a : α), l₁ = l₂
theorem list.subperm.cons_right {α : Type u_1} {l l' : list α} (x : α) (h : l <+~ l') :
l <+~ x :: l'
theorem list.subperm_append_diff_self_of_count_le {α : Type uu} [decidable_eq α] {l₁ l₂ : list α} (h : ∀ (x : α), x l₁ l₁ l₂) :
l₁ ++ l₂.diff l₁ ~ l₂

The list version of add_tsub_cancel_of_le for multisets.

theorem list.subperm_ext_iff {α : Type uu} [decidable_eq α] {l₁ l₂ : list α} :
l₁ <+~ l₂ ∀ (x : α), x l₁ l₁ l₂

The list version of multiset.le_iff_count.

@[simp]
theorem list.subperm_singleton_iff {α : Type u_1} {l : list α} {a : α} :
[a] <+~ l a l
theorem list.subperm.cons_left {α : Type uu} [decidable_eq α] {l₁ l₂ : list α} (h : l₁ <+~ l₂) (x : α) (hx : l₁ < l₂) :
x :: l₁ <+~ l₂
@[protected, instance]
def list.decidable_perm {α : Type uu} [decidable_eq α] (l₁ l₂ : list α) :
decidable (l₁ ~ l₂)
Equations
theorem list.perm.dedup {α : Type uu} [decidable_eq α] {l₁ l₂ : list α} (p : l₁ ~ l₂) :
l₁.dedup ~ l₂.dedup
theorem list.perm.insert {α : Type uu} [decidable_eq α] (a : α) {l₁ l₂ : list α} (p : l₁ ~ l₂) :
~
theorem list.perm_insert_swap {α : Type uu} [decidable_eq α] (x y : α) (l : list α) :
~
theorem list.perm_insert_nth {α : Type u_1} (x : α) (l : list α) {n : } (h : n l.length) :
l ~ x :: l
theorem list.perm.union_right {α : Type uu} [decidable_eq α] {l₁ l₂ : list α} (t₁ : list α) (h : l₁ ~ l₂) :
l₁ t₁ ~ l₂ t₁
theorem list.perm.union_left {α : Type uu} [decidable_eq α] (l : list α) {t₁ t₂ : list α} (h : t₁ ~ t₂) :
l t₁ ~ l t₂
theorem list.perm.union {α : Type uu} [decidable_eq α] {l₁ l₂ t₁ t₂ : list α} (p₁ : l₁ ~ l₂) (p₂ : t₁ ~ t₂) :
l₁ t₁ ~ l₂ t₂
theorem list.perm.inter_right {α : Type uu} [decidable_eq α] {l₁ l₂ : list α} (t₁ : list α) :
l₁ ~ l₂l₁ t₁ ~ l₂ t₁
theorem list.perm.inter_left {α : Type uu} [decidable_eq α] (l : list α) {t₁ t₂ : list α} (p : t₁ ~ t₂) :
l t₁ = l t₂
theorem list.perm.inter {α : Type uu} [decidable_eq α] {l₁ l₂ t₁ t₂ : list α} (p₁ : l₁ ~ l₂) (p₂ : t₁ ~ t₂) :
l₁ t₁ ~ l₂ t₂
theorem list.perm.inter_append {α : Type uu} [decidable_eq α] {l t₁ t₂ : list α} (h : t₁.disjoint t₂) :
l (t₁ ++ t₂) ~ l t₁ ++ l t₂
theorem list.perm.pairwise_iff {α : Type uu} {R : α → α → Prop} (S : symmetric R) {l₁ l₂ : list α} (p : l₁ ~ l₂) :
l₁ l₂
theorem list.pairwise.perm {α : Type uu} {R : α → α → Prop} {l l' : list α} (hR : l) (hl : l ~ l') (hsymm : symmetric R) :
l'
theorem list.perm.pairwise {α : Type uu} {R : α → α → Prop} {l l' : list α} (hl : l ~ l') (hR : l) (hsymm : symmetric R) :
l'
theorem list.perm.nodup_iff {α : Type uu} {l₁ l₂ : list α} :
l₁ ~ l₂(l₁.nodup l₂.nodup)
theorem list.perm.bind_right {α : Type uu} {β : Type vv} {l₁ l₂ : list α} (f : α → list β) (p : l₁ ~ l₂) :
l₁.bind f ~ l₂.bind f
theorem list.perm.bind_left {α : Type uu} {β : Type vv} (l : list α) {f g : α → list β} (h : ∀ (a : α), f a ~ g a) :
l.bind f ~ l.bind g
theorem list.bind_append_perm {α : Type uu} {β : Type vv} (l : list α) (f g : α → list β) :
l.bind f ++ l.bind g ~ l.bind (λ (x : α), f x ++ g x)
theorem list.map_append_bind_perm {α : Type uu} {β : Type vv} (l : list α) (f : α → β) (g : α → list β) :
l ++ l.bind g ~ l.bind (λ (x : α), f x :: g x)
theorem list.perm.product_right {α : Type uu} {β : Type vv} {l₁ l₂ : list α} (t₁ : list β) (p : l₁ ~ l₂) :
l₁ ×ˢ t₁ ~ l₂ ×ˢ t₁
theorem list.perm.product_left {α : Type uu} {β : Type vv} (l : list α) {t₁ t₂ : list β} (p : t₁ ~ t₂) :
l ×ˢ t₁ ~ l ×ˢ t₂
theorem list.perm.product {α : Type uu} {β : Type vv} {l₁ l₂ : list α} {t₁ t₂ : list β} (p₁ : l₁ ~ l₂) (p₂ : t₁ ~ t₂) :
l₁ ×ˢ t₁ ~ l₂ ×ˢ t₂
theorem list.sublists_cons_perm_append {α : Type uu} (a : α) (l : list α) :
theorem list.sublists_perm_sublists' {α : Type uu} (l : list α) :
theorem list.revzip_sublists {α : Type uu} (l l₁ l₂ : list α) :
(l₁, l₂) l.sublists.revzipl₁ ++ l₂ ~ l
theorem list.revzip_sublists' {α : Type uu} (l l₁ l₂ : list α) :
(l₁, l₂) l.sublists'.revzipl₁ ++ l₂ ~ l
theorem list.range_bind_sublists_len_perm {α : Type u_1} (l : list α) :
(list.range (l.length + 1)).bind (λ (n : ), ~ l.sublists'
theorem list.perm_lookmap {α : Type uu} (f : α → ) {l₁ l₂ : list α} (H : list.pairwise (λ (a b : α), ∀ (c : α), c f a∀ (d : α), d f ba = b c = d) l₁) (p : l₁ ~ l₂) :
l₁ ~ l₂
theorem list.perm.erasep {α : Type uu} (f : α → Prop) {l₁ l₂ : list α} (H : list.pairwise (λ (a b : α), f af bfalse) l₁) (p : l₁ ~ l₂) :
l₁ ~ l₂
theorem list.perm.take_inter {α : Type u_1} [decidable_eq α] {xs ys : list α} (n : ) (h : xs ~ ys) (h' : ys.nodup) :
xs ~ ys.inter xs)
theorem list.perm.drop_inter {α : Type u_1} [decidable_eq α] {xs ys : list α} (n : ) (h : xs ~ ys) (h' : ys.nodup) :
xs ~ ys.inter xs)
theorem list.perm.slice_inter {α : Type u_1} [decidable_eq α] {xs ys : list α} (n m : ) (h : xs ~ ys) (h' : ys.nodup) :
m xs ~ ys m xs
theorem list.perm_of_mem_permutations_aux {α : Type uu} {ts is l : list α} :
l ts.permutations_aux isl ~ ts ++ is
theorem list.perm_of_mem_permutations {α : Type uu} {l₁ l₂ : list α} (h : l₁ l₂.permutations) :
l₁ ~ l₂
theorem list.length_permutations_aux {α : Type uu} (ts is : list α) :
theorem list.length_permutations {α : Type uu} (l : list α) :
theorem list.mem_permutations_of_perm_lemma {α : Type uu} {is l : list α} (H : l ~ (∃ (ts' : list α) (H : ts' ~ list.nil), l = ts' ++ is) ) :
l ~ isl is.permutations
theorem list.mem_permutations_aux_of_perm {α : Type uu} {ts is l : list α} :
l ~ is ++ ts(∃ (is' : list α) (H : is' ~ is), l = is' ++ ts) l ts.permutations_aux is
@[simp]
theorem list.mem_permutations {α : Type uu} {s t : list α} :
s ~ t
theorem list.perm_permutations'_aux_comm {α : Type uu} (a b : α) (l : list α) :
theorem list.perm.permutations' {α : Type uu} {s t : list α} (p : s ~ t) :
theorem list.permutations_perm_permutations' {α : Type uu} (ts : list α) :
@[simp]
theorem list.mem_permutations' {α : Type uu} {s t : list α} :
s ~ t
theorem list.perm.permutations {α : Type uu} {s t : list α} (h : s ~ t) :
@[simp]
theorem list.perm_permutations_iff {α : Type uu} {s t : list α} :
s ~ t
@[simp]
theorem list.perm_permutations'_iff {α : Type uu} {s t : list α} :
s ~ t
theorem list.nth_le_permutations'_aux {α : Type uu} (s : list α) (x : α) (n : ) (hn : n < .length) :
.nth_le n hn = s
theorem list.count_permutations'_aux_self {α : Type uu} [decidable_eq α] (l : list α) (x : α) :
@[simp]
theorem list.length_permutations'_aux {α : Type uu} (s : list α) (x : α) :
@[simp]
theorem list.permutations'_aux_nth_le_zero {α : Type uu} (s : list α) (x : α) (hn : 0 < .length := _) :
.nth_le 0 hn = x :: s
theorem list.injective_permutations'_aux {α : Type uu} (x : α) :
theorem list.nodup_permutations'_aux_of_not_mem {α : Type uu} (s : list α) (x : α) (hx : x s) :
theorem list.nodup_permutations'_aux_iff {α : Type uu} {s : list α} {x : α} :
theorem list.nodup_permutations {α : Type uu} (s : list α) (hs : s.nodup) :