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.

def List.«term_~_» : Lean.TrailingParserDescr

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

Equations

• List.«term_~_» = Lean.ParserDescr.trailingNode `List.term_~_ 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ~ ") (Lean.ParserDescr.cat `term 51))

@[simp]

theorem List.Perm.refl {α : Type uu} (l : List α) : l ~ l

theorem List.Perm.symm {α : Type uu} {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) : l₂ ~ l₁

theorem List.perm_comm {α : Type uu} {l₁ : List α} {l₂ : List α} : l₁ ~ l₂ ↔ l₂ ~ l₁

theorem List.Perm.swap' {α : Type uu} (x : α) (y : α) {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) : y :: x :: l₁ ~ x :: y :: l₂

theorem List.Perm.eqv (α : Type u_1) : Equivalence List.Perm

theorem List.Perm.of_eq {α : Type uu} {l₁ : List α} {l₂ : List α} (h : l₁ = l₂) : l₁ ~ l₂

instance List.isSetoid (α : Type u_1) : Setoid (List α)

Equations

• List.isSetoid α = { r := List.Perm, iseqv := (_ : Equivalence List.Perm) }

theorem List.Perm.mem_iff {α : Type uu} {a : α} {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) : a ∈ l₁ ↔ a ∈ l₂

theorem List.Perm.subset {α : Type uu} {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) : l₁ ⊆ l₂

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

theorem List.Perm.subset_congr_right {α : Type uu} {l₁ : List α} {l₂ : List α} {l₃ : List α} (h : l₁ ~ l₂) : l₃ ⊆ l₁ ↔ l₃ ⊆ l₂

theorem List.Perm.append_right {α : Type uu} {l₁ : List α} {l₂ : List α} (t₁ : List α) (p : l₁ ~ l₂) : l₁ ++ t₁ ~ l₂ ++ t₁

theorem List.Perm.append_left {α : Type uu} {t₁ : List α} {t₂ : List α} (l : List α) : t₁ ~ t₂ → l ++ t₁ ~ l ++ t₂

theorem List.Perm.append {α : Type uu} {l₁ : List α} {l₂ : List α} {t₁ : List α} {t₂ : List α} (p₁ : l₁ ~ l₂) (p₂ : t₁ ~ t₂) : l₁ ++ t₁ ~ l₂ ++ t₂

theorem List.Perm.append_cons {α : Type uu} (a : α) {h₁ : List α} {h₂ : List α} {t₁ : List α} {t₂ : List α} (p₁ : h₁ ~ h₂) (p₂ : t₁ ~ t₂) : h₁ ++ a :: t₁ ~ h₂ ++ a :: t₂

@[simp]

theorem List.perm_middle {α : Type uu} {a : α} {l₁ : List α} {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₁ : List α} {l₂ : List α} : l₁ ++ l₂ ~ l₂ ++ l₁

theorem List.concat_perm {α : Type uu} (l : List α) (a : α) : List.concat l a ~ a :: l

theorem List.Perm.length_eq {α : Type uu} {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) : List.length l₁ = List.length l₂

theorem List.Perm.eq_nil {α : Type uu} {l : List α} (p : l ~ []) : l = []

theorem List.Perm.nil_eq {α : Type uu} {l : List α} (p : [] ~ l) : [] = l

@[simp]

theorem List.perm_nil {α : Type uu} {l₁ : List α} : l₁ ~ [] ↔ l₁ = []

@[simp]

theorem List.nil_perm {α : Type uu} {l₁ : List α} : [] ~ l₁ ↔ l₁ = []

theorem List.not_perm_nil_cons {α : Type uu} (x : α) (l : List α) : ¬[] ~ x :: l

@[simp]

theorem List.reverse_perm {α : Type uu} (l : List α) : List.reverse l ~ l

theorem List.perm_cons_append_cons {α : Type uu} {l : List α} {l₁ : List α} {l₂ : List α} (a : α) (p : l ~ l₁ ++ l₂) : a :: l ~ l₁ ++ a :: l₂

@[simp]

theorem List.perm_replicate {α : Type uu} {n : ℕ} {a : α} {l : List α} : l ~ List.replicate n a ↔ l = List.replicate n a

@[simp]

theorem List.replicate_perm {α : Type uu} {n : ℕ} {a : α} {l : List α} : List.replicate n a ~ l ↔ List.replicate n a = 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 α} : 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} [DecidableEq α] {a : α} {l : List α} (h : a ∈ l) : l ~ a :: List.erase l a

theorem List.perm_induction_on {α : Type uu} {P : List α → List α → Prop} {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) (h₁ : P [] []) (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.filterMap {α : Type uu} {β : Type vv} (f : α → Option β) {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) : List.filterMap f l₁ ~ List.filterMap f l₂

theorem List.Perm.map {α : Type uu} {β : Type vv} (f : α → β) {l₁ : List α} {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₁ : List α} {l₂ : List α} (p : 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 : α → Bool) {l₁ : List α} {l₂ : List α} (s : l₁ ~ l₂) : List.filter p l₁ ~ List.filter p l₂

theorem List.filter_append_perm {α : Type uu} (p : α → Bool) (l : List α) : List.filter p l ++ List.filter (fun x => decide ¬p x = true) l ~ l

theorem List.exists_perm_sublist {α : Type uu} {l₁ : List α} {l₂ : List α} {l₂' : List α} (s : List.Sublist l₁ l₂) (p : l₂ ~ l₂') : ∃ l₁' x, List.Sublist l₁' l₂'

theorem List.Perm.sizeOf_eq_sizeOf {α : Type uu} [SizeOf α] {l₁ : List α} {l₂ : List α} (h : l₁ ~ l₂) : sizeOf l₁ = sizeOf l₂

theorem List.perm_comp_perm {α : Type uu} : Relation.Comp List.Perm List.Perm = List.Perm

theorem List.perm_comp_forall₂ {α : Type uu} {β : Type vv} {r : α → β → Prop} {l : List α} {u : List α} {v : List β} (hlu : 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 uu} {β : Type vv} {r : α → β → Prop} : Relation.Comp (List.Forall₂ r) List.Perm = Relation.Comp List.Perm (List.Forall₂ r)

theorem List.rel_perm_imp {α : Type uu} {β : Type vv} {r : α → β → Prop} (hr : Relator.RightUnique r) : (List.Forall₂ r ⇒ List.Forall₂ r ⇒ fun x x_1 => x → x_1) List.Perm List.Perm

theorem List.rel_perm {α : Type uu} {β : Type vv} {r : α → β → Prop} (hr : Relator.BiUnique r) : (List.Forall₂ r ⇒ List.Forall₂ r ⇒ fun x x_1 => x ↔ x_1) List.Perm List.Perm

def List.Subperm {α : Type uu} (l₁ : List α) (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 x, List.Sublist l l₂

def List.«term_<+~_» : Lean.TrailingParserDescr

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

• List.«term_<+~_» = Lean.ParserDescr.trailingNode `List.term_<+~_ 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <+~ ") (Lean.ParserDescr.cat `term 51))

theorem List.nil_subperm {α : Type uu} {l : List α} : [] <+~ l

theorem List.Perm.subperm_left {α : Type uu} {l : List α} {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) : l <+~ l₁ ↔ l <+~ l₂

theorem List.Perm.subperm_right {α : Type uu} {l₁ : List α} {l₂ : List α} {l : List α} (p : l₁ ~ l₂) : l₁ <+~ l ↔ l₂ <+~ l

theorem List.Sublist.subperm {α : Type uu} {l₁ : List α} {l₂ : List α} (s : List.Sublist l₁ l₂) : l₁ <+~ l₂

theorem List.Perm.subperm {α : Type uu} {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) : l₁ <+~ l₂

theorem List.Subperm.refl {α : Type uu} (l : List α) : l <+~ l

theorem List.Subperm.trans {α : Type uu} {l₁ : List α} {l₂ : List α} {l₃ : List α} : l₁ <+~ l₂ → l₂ <+~ l₃ → l₁ <+~ l₃

theorem List.Subperm.length_le {α : Type uu} {l₁ : List α} {l₂ : List α} : l₁ <+~ l₂ → List.length l₁ ≤ List.length l₂

theorem List.Subperm.perm_of_length_le {α : Type uu} {l₁ : List α} {l₂ : List α} : l₁ <+~ l₂ → List.length l₂ ≤ List.length l₁ → l₁ ~ l₂

theorem List.Subperm.antisymm {α : Type uu} {l₁ : List α} {l₂ : List α} (h₁ : l₁ <+~ l₂) (h₂ : l₂ <+~ l₁) : l₁ ~ l₂

theorem List.Subperm.subset {α : Type uu} {l₁ : List α} {l₂ : List α} : l₁ <+~ l₂ → l₁ ⊆ l₂

theorem List.Subperm.filter {α : Type uu} (p : α → Bool) ⦃l : List α⦄ ⦃l' : List α⦄ (h : l <+~ l') : List.filter p l <+~ List.filter p l'

theorem List.Sublist.exists_perm_append {α : Type uu} {l₁ : List α} {l₂ : List α} : List.Sublist l₁ l₂ → ∃ l, l₂ ~ l₁ ++ l

theorem List.Perm.countP_eq {α : Type uu} (p : α → Bool) {l₁ : List α} {l₂ : List α} (s : l₁ ~ l₂) : List.countP p l₁ = List.countP p l₂

theorem List.Subperm.countP_le {α : Type uu} (p : α → Bool) {l₁ : List α} {l₂ : List α} : l₁ <+~ l₂ → List.countP p l₁ ≤ List.countP p l₂

theorem List.Perm.countP_congr {α : Type uu} {l₁ : List α} {l₂ : List α} (s : l₁ ~ l₂) {p : α → Bool} {p' : α → Bool} (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 : α → Bool) (q : α → Bool) : List.countP p l = List.countP p (List.filter q l) + List.countP p (List.filter (fun a => decide ¬q a = true) l)

theorem List.Perm.count_eq {α : Type uu} [DecidableEq α] {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) (a : α) : List.count a l₁ = List.count a l₂

theorem List.Subperm.count_le {α : Type uu} [DecidableEq α] {l₁ : List α} {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₁ : List α} {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₁ : List α} {l₂ : List α} (rcomm : RightCommutative 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₁ : List α} {l₂ : List α} (lcomm : LeftCommutative 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 : β []} {l : List α} {l' : List α} (hl : l ~ l') (f_congr : ∀ {a : α} {l l' : List α} {b : β l} {b' : β l'}, l ~ l' → HEq b b' → HEq (f a l b) (f a l' b')) (f_swap : ∀ {a a' : α} {l : List α} {b : β l}, HEq (f a (a' :: l) (f a' l b)) (f a' (a :: l) (f a l b))) : HEq (List.rec b f l) (List.rec b f l')

theorem List.Perm.fold_op_eq {α : Type uu} {op : α → α → α} [IA : IsAssociative α op] [IC : IsCommutative α op] {l₁ : List α} {l₂ : List α} {a : α} (h : l₁ ~ l₂) : List.foldl op a l₁ = List.foldl op a l₂

theorem List.Perm.sum_eq' {α : Type uu} [M : AddMonoid α] {l₁ : List α} {l₂ : List α} (h : 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 uu} [M : Monoid α] {l₁ : List α} {l₂ : List α} (h : 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 uu} [AddCommMonoid α] {l₁ : List α} {l₂ : List α} (h : l₁ ~ l₂) : List.sum l₁ = List.sum l₂

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

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

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

theorem List.perm_inv_core {α : Type uu} {a : α} {l₁ : List α} {l₂ : List α} {r₁ : List α} {r₂ : List α} : l₁ ++ a :: r₁ ~ l₂ ++ a :: r₂ → l₁ ++ r₁ ~ l₂ ++ r₂

theorem List.Perm.cons_inv {α : Type uu} {a : α} {l₁ : List α} {l₂ : List α} : a :: l₁ ~ a :: l₂ → l₁ ~ l₂

@[simp]

theorem List.perm_cons {α : Type uu} (a : α) {l₁ : List α} {l₂ : List α} : a :: l₁ ~ a :: l₂ ↔ l₁ ~ l₂

theorem List.perm_append_left_iff {α : Type uu} {l₁ : List α} {l₂ : List α} (l : List α) : l ++ l₁ ~ l ++ l₂ ↔ l₁ ~ l₂

theorem List.perm_append_right_iff {α : Type uu} {l₁ : List α} {l₂ : List α} (l : List α) : l₁ ++ l ~ l₂ ++ l ↔ l₁ ~ l₂

theorem List.perm_option_to_list {α : Type uu} {o₁ : Option α} {o₂ : Option α} : Option.toList o₁ ~ Option.toList o₂ ↔ o₁ = o₂

theorem List.subperm_cons {α : Type uu} (a : α) {l₁ : List α} {l₂ : List α} : a :: l₁ <+~ a :: l₂ ↔ l₁ <+~ l₂

theorem List.subperm.cons {α : Type uu} (a : α) {l₁ : List α} {l₂ : List α} : l₁ <+~ l₂ → a :: l₁ <+~ a :: l₂

Alias of the reverse direction of List.subperm_cons.

theorem List.subperm.of_cons {α : Type uu} (a : α) {l₁ : List α} {l₂ : List α} : a :: l₁ <+~ a :: l₂ → l₁ <+~ l₂

Alias of the forward direction of List.subperm_cons.

theorem List.cons_subperm_of_mem {α : Type uu} {a : α} {l₁ : List α} {l₂ : List α} (d₁ : List.Nodup l₁) (h₁ : ¬a ∈ l₁) (h₂ : a ∈ l₂) (s : l₁ <+~ l₂) : a :: l₁ <+~ l₂

theorem List.subperm_append_left {α : Type uu} {l₁ : List α} {l₂ : List α} (l : List α) : l ++ l₁ <+~ l ++ l₂ ↔ l₁ <+~ l₂

theorem List.subperm_append_right {α : Type uu} {l₁ : List α} {l₂ : List α} (l : List α) : l₁ ++ l <+~ l₂ ++ l ↔ l₁ <+~ l₂

theorem List.Subperm.exists_of_length_lt {α : Type uu} {l₁ : List α} {l₂ : List α} : l₁ <+~ l₂ → List.length l₁ < List.length l₂ → ∃ a, a :: l₁ <+~ l₂

theorem List.Nodup.subperm {α : Type uu} {l₁ : List α} {l₂ : List α} (d : List.Nodup l₁) (H : l₁ ⊆ l₂) : l₁ <+~ l₂

theorem List.perm_ext {α : Type uu} {l₁ : List α} {l₂ : List α} (d₁ : List.Nodup l₁) (d₂ : List.Nodup l₂) : l₁ ~ l₂ ↔ ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂

theorem List.Nodup.sublist_ext {α : Type uu} {l₁ : List α} {l₂ : List α} {l : List α} (d : List.Nodup l) (s₁ : List.Sublist l₁ l) (s₂ : List.Sublist l₂ l) : l₁ ~ l₂ ↔ l₁ = l₂

theorem List.Perm.erase {α : Type uu} [DecidableEq α] (a : α) {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) : List.erase l₁ a ~ List.erase l₂ a

theorem List.subperm_cons_erase {α : Type uu} [DecidableEq α] (a : α) (l : List α) : l <+~ a :: List.erase l a

theorem List.erase_subperm {α : Type uu} [DecidableEq α] (a : α) (l : List α) : List.erase l a <+~ l

theorem List.Subperm.erase {α : Type uu} [DecidableEq α] {l₁ : List α} {l₂ : List α} (a : α) (h : l₁ <+~ l₂) : List.erase l₁ a <+~ List.erase l₂ a

theorem List.Perm.diff_right {α : Type uu} [DecidableEq α] {l₁ : List α} {l₂ : List α} (t : List α) (h : l₁ ~ l₂) : List.diff l₁ t ~ List.diff l₂ t

theorem List.Perm.diff_left {α : Type uu} [DecidableEq α] (l : List α) {t₁ : List α} {t₂ : List α} (h : t₁ ~ t₂) : List.diff l t₁ = List.diff l t₂

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

theorem List.Subperm.diff_right {α : Type uu} [DecidableEq α] {l₁ : List α} {l₂ : List α} (h : l₁ <+~ l₂) (t : List α) : List.diff l₁ t <+~ List.diff l₂ t

theorem List.erase_cons_subperm_cons_erase {α : Type uu} [DecidableEq α] (a : α) (b : α) (l : List α) : List.erase (a :: l) b <+~ a :: List.erase l b

theorem List.subperm_cons_diff {α : Type uu} [DecidableEq α] {a : α} {l₁ : List α} {l₂ : List α} : List.diff (a :: l₁) l₂ <+~ a :: List.diff l₁ l₂

theorem List.subset_cons_diff {α : Type uu} [DecidableEq α] {a : α} {l₁ : List α} {l₂ : List α} : List.diff (a :: l₁) l₂ ⊆ a :: List.diff l₁ l₂

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

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

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

theorem List.cons_perm_iff_perm_erase {α : Type uu} [DecidableEq α] {a : α} {l₁ : List α} {l₂ : List α} : a :: l₁ ~ l₂ ↔ a ∈ l₂ ∧ l₁ ~ List.erase l₂ a

theorem List.perm_iff_count {α : Type uu} [DecidableEq α] {l₁ : List α} {l₂ : List α} : l₁ ~ l₂ ↔ ∀ (a : α), List.count a l₁ = List.count a l₂

theorem List.perm_replicate_append_replicate {α : Type uu} [DecidableEq α] {l : List α} {a : α} {b : α} {m : ℕ} {n : ℕ} (h : a ≠ b) : l ~ List.replicate m a ++ List.replicate n b ↔ List.count a l = m ∧ List.count b l = n ∧ l ⊆ [a, b]

theorem List.Subperm.cons_right {α : Type u_1} {l : List α} {l' : List α} (x : α) (h : l <+~ l') : l <+~ x :: l'

theorem List.subperm_append_diff_self_of_count_le {α : Type uu} [DecidableEq α] {l₁ : List α} {l₂ : List α} (h : ∀ (x : α), x ∈ l₁ → List.count x l₁ ≤ List.count x l₂) : l₁ ++ List.diff l₂ l₁ ~ l₂

The list version of add_tsub_cancel_of_le for multisets.

theorem List.subperm_ext_iff {α : Type uu} [DecidableEq α] {l₁ : List α} {l₂ : List α} : l₁ <+~ l₂ ↔ ∀ (x : α), x ∈ l₁ → List.count x l₁ ≤ List.count x l₂

The list version of Multiset.le_iff_count.

instance List.decidableSubperm {α : Type uu} [DecidableEq α] : DecidableRel fun x x_1 => x <+~ x_1

Equations

• List.decidableSubperm x x = decidable_of_iff (∀ (x : α), x ∈ x → List.count x x ≤ List.count x x) (_ : (∀ (x : α), x ∈ x → List.count x x ≤ List.count x x) ↔ x <+~ x)

@[simp]

theorem List.subperm_singleton_iff {α : Type u_1} {l : List α} {a : α} : [a] <+~ l ↔ a ∈ l

theorem List.Subperm.cons_left {α : Type uu} [DecidableEq α] {l₁ : List α} {l₂ : List α} (h : l₁ <+~ l₂) (x : α) (hx : List.count x l₁ < List.count x l₂) : x :: l₁ <+~ l₂

instance List.decidablePerm {α : Type uu} [DecidableEq α] (l₁ : List α) (l₂ : List α) : Decidable (l₁ ~ l₂)

Equations

• List.decidablePerm [] [] = isTrue (_ : [] ~ [])
• List.decidablePerm [] (b :: l₂) = isFalse (_ : [] ~ b :: l₂ → List.noConfusionType False [] (b :: l₂))
• List.decidablePerm (a :: l₁) x = decidable_of_iff' (a ∈ x ∧ l₁ ~ List.erase x a) (_ : a :: l₁ ~ x ↔ a ∈ x ∧ l₁ ~ List.erase x a)

theorem List.Perm.dedup {α : Type uu} [DecidableEq α] {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) : List.dedup l₁ ~ List.dedup l₂

theorem List.Perm.insert {α : Type uu} [DecidableEq α] (a : α) {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) : List.insert a l₁ ~ List.insert a l₂

theorem List.perm_insert_swap {α : Type uu} [DecidableEq α] (x : α) (y : α) (l : List α) : List.insert x (List.insert y l) ~ List.insert y (List.insert x l)

theorem List.perm_insertNth {α : Type u_1} (x : α) (l : List α) {n : ℕ} (h : n ≤ List.length l) : List.insertNth n x l ~ x :: l

theorem List.Perm.union_right {α : Type uu} [DecidableEq α] {l₁ : List α} {l₂ : List α} (t₁ : List α) (h : l₁ ~ l₂) : l₁ ∪ t₁ ~ l₂ ∪ t₁

theorem List.Perm.union_left {α : Type uu} [DecidableEq α] (l : List α) {t₁ : List α} {t₂ : List α} (h : t₁ ~ t₂) : l ∪ t₁ ~ l ∪ t₂

theorem List.Perm.union {α : Type uu} [DecidableEq α] {l₁ : List α} {l₂ : List α} {t₁ : List α} {t₂ : List α} (p₁ : l₁ ~ l₂) (p₂ : t₁ ~ t₂) : l₁ ∪ t₁ ~ l₂ ∪ t₂

theorem List.Perm.inter_right {α : Type uu} [DecidableEq α] {l₁ : List α} {l₂ : List α} (t₁ : List α) : l₁ ~ l₂ → l₁ ∩ t₁ ~ l₂ ∩ t₁

theorem List.Perm.inter_left {α : Type uu} [DecidableEq α] (l : List α) {t₁ : List α} {t₂ : List α} (p : t₁ ~ t₂) : l ∩ t₁ = l ∩ t₂

theorem List.Perm.inter {α : Type uu} [DecidableEq α] {l₁ : List α} {l₂ : List α} {t₁ : List α} {t₂ : List α} (p₁ : l₁ ~ l₂) (p₂ : t₁ ~ t₂) : l₁ ∩ t₁ ~ l₂ ∩ t₂

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

theorem List.Perm.pairwise_iff {α : Type uu} {R : α → α → Prop} (S : Symmetric R) {l₁ : List α} {l₂ : List α} (_p : l₁ ~ l₂) : List.Pairwise R l₁ ↔ List.Pairwise R l₂

theorem List.Pairwise.perm {α : Type uu} {R : α → α → Prop} {l : List α} {l' : List α} (hR : List.Pairwise R l) (hl : l ~ l') (hsymm : Symmetric R) : List.Pairwise R l'

theorem List.Perm.pairwise {α : Type uu} {R : α → α → Prop} {l : List α} {l' : List α} (hl : l ~ l') (hR : List.Pairwise R l) (hsymm : Symmetric R) : List.Pairwise R l'

theorem List.Perm.nodup_iff {α : Type uu} {l₁ : List α} {l₂ : List α} : l₁ ~ l₂ → (List.Nodup l₁ ↔ List.Nodup l₂)

theorem List.Perm.join {α : Type uu} {l₁ : List (List α)} {l₂ : List (List α)} (h : l₁ ~ l₂) : List.join l₁ ~ List.join l₂

theorem List.Perm.bind_right {α : Type uu} {β : Type vv} {l₁ : List α} {l₂ : List α} (f : α → List β) (p : l₁ ~ l₂) : List.bind l₁ f ~ List.bind l₂ f

theorem List.Perm.join_congr {α : Type uu} {l₁ : List (List α)} {l₂ : List (List α)} : List.Forall₂ (fun x x_1 => x ~ x_1) l₁ l₂ → List.join l₁ ~ List.join l₂

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

theorem List.bind_append_perm {α : Type uu} {β : Type vv} (l : List α) (f : α → List β) (g : α → List β) : List.bind l f ++ List.bind l g ~ List.bind l fun x => f x ++ g x

theorem List.map_append_bind_perm {α : Type uu} {β : Type vv} (l : List α) (f : α → β) (g : α → List β) : List.map f l ++ List.bind l g ~ List.bind l fun x => f x :: g x

theorem List.Perm.product_right {α : Type uu} {β : Type vv} {l₁ : List α} {l₂ : List α} (t₁ : List β) (p : l₁ ~ l₂) : List.product l₁ t₁ ~ List.product l₂ t₁

theorem List.Perm.product_left {α : Type uu} {β : Type vv} (l : List α) {t₁ : List β} {t₂ : List β} (p : t₁ ~ t₂) : List.product l t₁ ~ List.product l t₂

theorem List.Perm.product {α : Type uu} {β : Type vv} {l₁ : List α} {l₂ : List α} {t₁ : List β} {t₂ : List β} (p₁ : l₁ ~ l₂) (p₂ : t₁ ~ t₂) : List.product l₁ t₁ ~ List.product l₂ t₂

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

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

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

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

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

theorem List.perm_of_mem_permutationsAux {α : Type uu} {ts : List α} {is : List α} {l : List α} : l ∈ List.permutationsAux ts is → l ~ ts ++ is

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

theorem List.length_permutationsAux {α : Type uu} (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 uu} (l : List α) : List.length (List.permutations l) = Nat.factorial (List.length l)

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

theorem List.mem_permutationsAux_of_perm {α : Type uu} {ts : List α} {is : List α} {l : List α} : l ~ is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ List.permutationsAux ts is

@[simp]

theorem List.mem_permutations {α : Type uu} {s : List α} {t : List α} : s ∈ List.permutations t ↔ s ~ t

theorem List.perm_permutations'Aux_comm {α : Type uu} (a : α) (b : α) (l : List α) : 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 uu} {s : List α} {t : List α} (p : s ~ t) : List.permutations' s ~ List.permutations' t

theorem List.permutations_perm_permutations' {α : Type uu} (ts : List α) : List.permutations ts ~ List.permutations' ts

@[simp]

theorem List.mem_permutations' {α : Type uu} {s : List α} {t : List α} : s ∈ List.permutations' t ↔ s ~ t

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

@[simp]

theorem List.perm_permutations_iff {α : Type uu} {s : List α} {t : List α} : List.permutations s ~ List.permutations t ↔ s ~ t

@[simp]

theorem List.perm_permutations'_iff {α : Type uu} {s : List α} {t : List α} : List.permutations' s ~ List.permutations' t ↔ s ~ t

theorem List.nthLe_permutations'Aux {α : Type uu} (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 uu} [DecidableEq α] (l : List α) (x : α) : List.count (x :: l) (List.permutations'Aux x l) = List.length (List.takeWhile (fun b => decide ((fun x x_1 => x = x_1) x b)) l) + 1

@[simp]

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

@[simp]

theorem List.permutations'Aux_nthLe_zero {α : Type uu} (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 uu} (x : α) : Function.Injective (List.permutations'Aux x)

theorem List.nodup_permutations'Aux_of_not_mem {α : Type uu} (s : List α) (x : α) (hx : ¬x ∈ s) : List.Nodup (List.permutations'Aux x s)

theorem List.nodup_permutations'Aux_iff {α : Type uu} {s : List α} {x : α} : List.Nodup (List.permutations'Aux x s) ↔ ¬x ∈ s

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