mathlib3 documentation

data.list.perm

List Permutations #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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₂
@[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.subset_congr_left {α : Type uu} {l₁ l₂ l₃ : list α} (h : l₁ ~ l₂) :
l₁ l₃ l₂ l₃
theorem list.perm.subset_congr_right {α : Type uu} {l₁ l₂ l₃ : list α} (h : l₁ ~ l₂) :
l₃ l₁ l₃ 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 α} :
l₁ ~ list.nil l₁ = list.nil
@[simp]
theorem list.nil_perm {α : Type uu} {l₁ : list α} :
list.nil ~ l₁ l₁ = list.nil
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_replicate {α : Type uu} {n : } {a : α} {l : list α} :
@[simp]
theorem list.replicate_perm {α : Type uu} {n : } {a : α} {l : list α} :
@[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 α} :
l ~ [a] l = [a]

Alias of the forward direction of list.perm_singleton.

theorem list.perm.singleton_eq {α : Type uu} {a : α} {l : list α} :
[a] ~ l [a] = l

Alias of the forward direction of list.singleton_perm.

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₁ : P list.nil 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 : α option β) {l₁ l₂ : list α} (p : l₁ ~ l₂) :
theorem list.perm.map {α : Type uu} {β : Type vv} (f : α β) {l₁ l₂ : list α} (p : l₁ ~ l₂) :
list.map f l₁ ~ list.map f 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} :
list.pmap f l₁ H₁ ~ list.pmap f l₂ H₂
theorem list.perm.filter {α : Type uu} (p : α Prop) [decidable_pred p] {l₁ l₂ : list α} (s : l₁ ~ l₂) :
list.filter p l₁ ~ list.filter p l₂
theorem list.filter_append_perm {α : Type uu} (p : α Prop) [decidable_pred p] (l : list α) :
list.filter p 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_forall₂ {α : Type uu} {β : Type vv} {r : α β Prop} {l u : list α} {v : list β} (hlu : l ~ u) (huv : list.forall₂ r u v) :
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
Instances for list.subperm
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₁.length l₁ ~ 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) [decidable_pred p] ⦃l l' : list α⦄ (h : 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) [decidable_pred p] {l₁ l₂ : list α} (s : l₁ ~ l₂) :
list.countp p l₁ = list.countp p l₂
theorem list.subperm.countp_le {α : Type uu} (p : α Prop) [decidable_pred p] {l₁ l₂ : list α} :
l₁ <+~ l₂ list.countp p l₁ list.countp p l₂
theorem list.perm.countp_congr {α : Type uu} {l₁ l₂ : list α} (s : l₁ ~ l₂) {p p' : α Prop} [decidable_pred p] [decidable_pred p'] (hp : (x : α), x l₁ (p x p' x)) :
list.countp p l₁ = list.countp p' l₂
theorem list.countp_eq_countp_filter_add {α : Type uu} (l : list α) (p q : α Prop) [decidable_pred p] [decidable_pred q] :
list.countp p l = list.countp p (list.filter q l) + list.countp p (list.filter (λ (a : α), ¬q a) l)
theorem list.perm.count_eq {α : Type uu} [decidable_eq α] {l₁ l₂ : list α} (p : l₁ ~ l₂) (a : α) :
list.count a l₁ = list.count a l₂
theorem list.subperm.count_le {α : Type uu} [decidable_eq α] {l₁ l₂ : list α} (s : l₁ <+~ l₂) (a : α) :
list.count a l₁ list.count a 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 : β), list.foldl f b l₁ = list.foldl f b l₂
theorem list.perm.foldl_eq {α : Type uu} {β : Type vv} {f : β α β} {l₁ l₂ : list α} (rcomm : right_commutative f) (p : l₁ ~ l₂) (b : β) :
list.foldl f b l₁ = list.foldl f b l₂
theorem list.perm.foldr_eq {α : Type uu} {β : Type vv} {f : α β β} {l₁ l₂ : list α} (lcomm : left_commutative f) (p : l₁ ~ l₂) (b : β) :
list.foldr f b l₁ = list.foldr f 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 : α α α} [is_associative α op] [is_commutative α op] {l₁ l₂ : list α} {a : α} (h : l₁ ~ l₂) :
list.foldl op a l₁ = list.foldl op a l₂
theorem list.perm.prod_eq' {α : Type uu} [monoid α] {l₁ l₂ : list α} (h : l₁ ~ l₂) (hc : list.pairwise commute 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 add_commute l₁) :
l₁.sum = l₂.sum

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 uu} [comm_monoid α] {l₁ l₂ : list α} (h : l₁ ~ l₂) :
l₁.prod = l₂.prod
theorem list.perm.sum_eq {α : Type uu} [add_comm_monoid α] {l₁ l₂ : list α} (h : l₁ ~ l₂) :
l₁.sum = l₂.sum
theorem list.sum_reverse {α : Type uu} [add_comm_monoid α] (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 : α), list.count a l₁ = list.count a l₂
theorem list.perm_replicate_append_replicate {α : Type uu} [decidable_eq α] {l : list α} {a b : α} {m n : } (h : a b) :
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₁ list.count x l₁ list.count x 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₁ list.count x l₁ list.count x l₂

The list version of multiset.le_iff_count.

@[protected, instance]
Equations
@[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 : list.count x l₁ < list.count x 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_nth {α : Type u_1} (x : α) (l : list α) {n : } (h : n l.length) :
list.insert_nth n x 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₂) :
theorem list.pairwise.perm {α : Type uu} {R : α α Prop} {l l' : list α} (hR : list.pairwise R l) (hl : l ~ l') (hsymm : symmetric R) :
theorem list.perm.pairwise {α : Type uu} {R : α α Prop} {l l' : list α} (hl : l ~ l') (hR : list.pairwise R l) (hsymm : symmetric R) :
theorem list.perm.nodup_iff {α : Type uu} {l₁ l₂ : list α} :
l₁ ~ l₂ (l₁.nodup l₂.nodup)
theorem list.perm.join {α : Type uu} {l₁ l₂ : list (list α)} (h : l₁ ~ l₂) :
l₁.join ~ l₂.join
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.join_congr {α : Type uu} {l₁ l₂ : list (list α)} (h : list.forall₂ list.perm l₁ l₂) :
l₁.join ~ l₂.join
theorem list.perm.bind_left {α : Type uu} {β : Type vv} (l : list α) {f g : α list β} (h : (a : α), a l 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 β) :
list.map f 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.perm_lookmap {α : Type uu} (f : α option α) {l₁ l₂ : list α} (H : list.pairwise (λ (a b : α), (c : α), c f a (d : α), d f b a = b c = d) l₁) (p : l₁ ~ l₂) :
theorem list.perm.erasep {α : Type uu} (f : α Prop) [decidable_pred f] {l₁ l₂ : list α} (H : list.pairwise (λ (a b : α), f a f b false) l₁) (p : l₁ ~ l₂) :
list.erasep f l₁ ~ list.erasep f l₂
theorem list.perm.take_inter {α : Type u_1} [decidable_eq α] {xs ys : list α} (n : ) (h : xs ~ ys) (h' : ys.nodup) :
list.take n xs ~ ys.inter (list.take n xs)
theorem list.perm.drop_inter {α : Type u_1} [decidable_eq α] {xs ys : list α} (n : ) (h : xs ~ ys) (h' : ys.nodup) :
list.drop n xs ~ ys.inter (list.drop n xs)
theorem list.perm.slice_inter {α : Type u_1} [decidable_eq α] {xs ys : list α} (n m : ) (h : xs ~ ys) (h' : ys.nodup) :
list.slice n m xs ~ ys list.slice n m xs
theorem list.perm_of_mem_permutations_aux {α : Type uu} {ts is l : list α} :
l ts.permutations_aux is l ~ ts ++ is
theorem list.perm_of_mem_permutations {α : Type uu} {l₁ l₂ : list α} (h : l₁ l₂.permutations) :
l₁ ~ l₂
theorem list.mem_permutations_of_perm_lemma {α : Type uu} {is l : list α} (H : l ~ list.nil ++ is ( (ts' : list α) (H : ts' ~ list.nil), l = ts' ++ is) l is.permutations_aux list.nil) :
l ~ is l 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 α} :
theorem list.perm.permutations' {α : Type uu} {s t : list α} (p : s ~ t) :
@[simp]
theorem list.mem_permutations' {α : Type uu} {s t : list α} :
theorem list.perm.permutations {α : Type uu} {s t : list α} (h : s ~ t) :
@[simp]
theorem list.perm_permutations_iff {α : Type uu} {s t : list α} :
@[simp]
theorem list.perm_permutations'_iff {α : Type uu} {s t : list α} :
theorem list.nth_le_permutations'_aux {α : Type uu} (s : list α) (x : α) (n : ) (hn : n < (list.permutations'_aux x s).length) :
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 < (list.permutations'_aux x s).length := _) :
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) :