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.

@[simp]

theorem List.nil_subperm {α : Type u_1} {l : List α} : [].Subperm l

theorem List.Perm.subperm_left {α : Type u_1} {l l₁ l₂ : List α} (p : l₁.Perm l₂) : l.Subperm l₁ ↔ l.Subperm l₂

theorem List.Perm.subperm_right {α : Type u_1} {l₁ l₂ l : List α} (p : l₁.Perm l₂) : l₁.Subperm l ↔ l₂.Subperm l

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

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

theorem List.Subperm.refl {α : Type u_1} (l : List α) : l.Subperm l

theorem List.Subperm.trans {α : Type u_1} {l₁ l₂ l₃ : List α} (s₁₂ : l₁.Subperm l₂) (s₂₃ : l₂.Subperm l₃) : l₁.Subperm l₃

theorem List.Subperm.cons_self {α✝ : Type u_1} {l : List α✝} {a : α✝} : l.Subperm (a :: l)

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

theorem List.Subperm.length_le {α : Type u_1} {l₁ l₂ : List α} : l₁.Subperm l₂ → l₁.length ≤ l₂.length

theorem List.Subperm.perm_of_length_le {α : Type u_1} {l₁ l₂ : List α} : l₁.Subperm l₂ → l₂.length ≤ l₁.length → l₁.Perm l₂

theorem List.Subperm.antisymm {α : Type u_1} {l₁ l₂ : List α} (h₁ : l₁.Subperm l₂) (h₂ : l₂.Subperm l₁) : l₁.Perm l₂

theorem List.Subperm.subset {α : Type u_1} {l₁ l₂ : List α} : l₁.Subperm l₂ → l₁ ⊆ l₂

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

@[simp]

theorem List.subperm_nil {α✝ : Type u_1} {l : List α✝} : l.Subperm [] ↔ l = []

@[simp]

theorem List.singleton_subperm_iff {α : Type u_1} {l : List α} {a : α} : [a].Subperm l ↔ a ∈ l

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

theorem List.Subperm.count_le {α : Type u_1} [BEq α] {l₁ l₂ : List α} (s : l₁.Subperm l₂) (a : α) : count a l₁ ≤ count a l₂

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

theorem List.cons_subperm_of_not_mem_of_mem {α : Type u_1} {a : α} {l₁ l₂ : List α} (h₁ : ¬a ∈ l₁) (h₂ : a ∈ l₂) (s : l₁.Subperm l₂) : (a :: l₁).Subperm l₂

Weaker version of Subperm.cons_left

theorem List.subperm_append_left {α : Type u_1} {l₁ l₂ : List α} (l : List α) : (l ++ l₁).Subperm (l ++ l₂) ↔ l₁.Subperm l₂

theorem List.subperm_append_right {α : Type u_1} {l₁ l₂ : List α} (l : List α) : (l₁ ++ l).Subperm (l₂ ++ l) ↔ l₁.Subperm l₂

theorem List.Subperm.exists_of_length_lt {α : Type u_1} {l₁ l₂ : List α} (s : l₁.Subperm l₂) (h : l₁.length < l₂.length) : ∃ (a : α), (a :: l₁).Subperm l₂

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

theorem List.perm_ext_iff_of_nodup {α : Type u_1} {l₁ l₂ : List α} (d₁ : l₁.Nodup) (d₂ : l₂.Nodup) : l₁.Perm l₂ ↔ ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂

theorem List.Nodup.perm_iff_eq_of_sublist {α : Type u_1} {l₁ l₂ l : List α} (d : l.Nodup) (s₁ : l₁.Sublist l) (s₂ : l₂.Sublist l) : l₁.Perm l₂ ↔ l₁ = l₂

theorem List.subperm_cons_erase {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (l : List α) : l.Subperm (a :: l.erase a)

theorem List.erase_subperm {α : Type u_1} [BEq α] (a : α) (l : List α) : (l.erase a).Subperm l

theorem List.Subperm.erase {α : Type u_1} {l₁ l₂ : List α} [BEq α] [LawfulBEq α] (a : α) (h : l₁.Subperm l₂) : (l₁.erase a).Subperm (l₂.erase a)

theorem List.Perm.diff_right {α : Type u_1} {l₁ l₂ : List α} [BEq α] [LawfulBEq α] (t : List α) (h : l₁.Perm l₂) : (l₁.diff t).Perm (l₂.diff t)

theorem List.Perm.diff_left {α : Type u_1} {t₁ t₂ : List α} [BEq α] [LawfulBEq α] (l : List α) (h : t₁.Perm t₂) : l.diff t₁ = l.diff t₂

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

theorem List.Subperm.diff_right {α : Type u_1} {l₁ l₂ : List α} [BEq α] [LawfulBEq α] (h : l₁.Subperm l₂) (t : List α) : (l₁.diff t).Subperm (l₂.diff t)

theorem List.erase_cons_subperm_cons_erase {α : Type u_1} [BEq α] [LawfulBEq α] (a b : α) (l : List α) : ((a :: l).erase b).Subperm (a :: l.erase b)

theorem List.subperm_cons_diff {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l₁ l₂ : List α} : ((a :: l₁).diff l₂).Subperm (a :: l₁.diff l₂)

theorem List.subset_cons_diff {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l₁ l₂ : List α} : (a :: l₁).diff l₂ ⊆ a :: l₁.diff l₂

theorem List.subperm_append_diff_self_of_count_le {α : Type u_1} [BEq α] [LawfulBEq α] {l₁ l₂ : List α} (h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂) : (l₁ ++ l₂.diff l₁).Perm l₂

The list version of add_tsub_cancel_of_le for multisets.

theorem List.subperm_ext_iff {α : Type u_1} [BEq α] [LawfulBEq α] {l₁ l₂ : List α} : l₁.Subperm l₂ ↔ ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂

The list version of Multiset.le_iff_count.

theorem List.isSubperm_iff {α : Type u_1} [BEq α] [LawfulBEq α] {l₁ l₂ : List α} : l₁.isSubperm l₂ = true ↔ l₁.Subperm l₂

instance List.decidableSubperm {α : Type u_1} [BEq α] [LawfulBEq α] : DecidableRel fun (x1 x2 : List α) => x1.Subperm x2

Equations

• x✝¹.decidableSubperm x✝ = decidable_of_iff (x✝¹.isSubperm x✝ = true) ⋯

theorem List.Subperm.cons_left {α : Type u_1} {l₁ l₂ : List α} [BEq α] [LawfulBEq α] (h : l₁.Subperm l₂) (x : α) (hx : count x l₁ < count x l₂) : (x :: l₁).Subperm l₂

theorem List.Perm.union_right {α : Type u_1} {l₁ l₂ : List α} [BEq α] [LawfulBEq α] (t₁ : List α) (h : l₁.Perm l₂) : (l₁ ∪ t₁).Perm (l₂ ∪ t₁)

theorem List.Perm.union_left {α : Type u_1} {t₁ t₂ : List α} [BEq α] [LawfulBEq α] (l : List α) (h : t₁.Perm t₂) : (l ∪ t₁).Perm (l ∪ t₂)

theorem List.Perm.union {α : Type u_1} [BEq α] [LawfulBEq α] {l₁ l₂ t₁ t₂ : List α} (p₁ : l₁.Perm l₂) (p₂ : t₁.Perm t₂) : (l₁ ∪ t₁).Perm (l₂ ∪ t₂)

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

theorem List.Perm.inter_left {α : Type u_1} {t₁ t₂ : List α} [BEq α] [LawfulBEq α] (l : List α) (p : t₁.Perm t₂) : l ∩ t₁ = l ∩ t₂

theorem List.Perm.inter {α : Type u_1} [BEq α] [LawfulBEq α] {l₁ l₂ t₁ t₂ : List α} (p₁ : l₁.Perm l₂) (p₂ : t₁.Perm t₂) : (l₁ ∩ t₁).Perm (l₂ ∩ t₂)

theorem List.Perm.flatten_congr {α : Type u_1} {l₁ l₂ : List (List α)} : Forall₂ (fun (x1 x2 : List α) => x1.Perm x2) l₁ l₂ → l₁.flatten.Perm l₂.flatten

theorem List.perm_insertP {α : Type u_1} (p : α → Bool) (a : α) (l : List α) : (insertP p a l).Perm (a :: l)

theorem List.Perm.insertP {α : Type u_1} {l₁ l₂ : List α} (p : α → Bool) (a : α) (h : l₁.Perm l₂) : (List.insertP p a l₁).Perm (List.insertP p a l₂)

idxBij

@[simp]

theorem List.Subperm.countBefore_idxOfNth {α : Type u_1} {i : Nat} [BEq α] [ReflBEq α] {xs ys : List α} (h : xs.Subperm ys) {hi : i < xs.length} : countBefore xs[i] ys (idxOfNth xs[i] ys (countBefore xs[i] xs i)) = countBefore xs[i] xs i

@[simp]

theorem List.Sublist.countBefore_idxOfNth {α : Type u_1} {i : Nat} [BEq α] [ReflBEq α] {xs ys : List α} (h : xs.Sublist ys) {hi : i < xs.length} : countBefore xs[i] ys (idxOfNth xs[i] ys (countBefore xs[i] xs i)) = countBefore xs[i] xs i

@[simp]

theorem List.Perm.countBefore_idxOfNth {α : Type u_1} {i : Nat} [BEq α] [ReflBEq α] {xs ys : List α} (h : xs.Perm ys) {hi : i < xs.length} : countBefore xs[i] ys (idxOfNth xs[i] ys (countBefore xs[i] xs i)) = countBefore xs[i] xs i

def List.Subperm.idxInj {α : Type u_1} [BEq α] [ReflBEq α] {xs ys : List α} (h : xs.Subperm ys) (i : Fin xs.length) : Fin ys.length

Subperm.idxInj is an injective map from Fin xs.length to Fin ys.length which exists when we have xs <+~ ys: conceptually it represents an embedding of one list into the other. For example:

(by decide : [1, 0, 1] <+~ [5, 0, 1, 3, 1]).idxInj 1 = 1

Equations

• h.idxInj i = match xs.idxToSigmaCount i with | ⟨x, t⟩ => ys.sigmaCountToIdx ⟨x, ⟨↑t, ⋯⟩⟩

@[simp]

theorem List.coe_idxInj {α : Type u_1} [BEq α] [ReflBEq α] {xs ys : List α} {h : xs.Subperm ys} {i : Fin xs.length} : ↑(h.idxInj i) = idxOfNth xs[i] ys (countBefore xs[i] xs ↑i)

theorem List.Subperm.getElem_idxInj_eq_getElem {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} (h : xs.Subperm ys) {i : Fin xs.length} : ys[↑(h.idxInj i)] = xs[↑i]

theorem List.Subperm.idxInj_injective {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} (h : xs.Subperm ys) : Function.Injective h.idxInj

@[simp]

theorem List.Subperm.idxInj_inj {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} {h : xs.Subperm ys} (i j : Fin xs.length) : h.idxInj i = h.idxInj j ↔ i = j

def List.Sublist.idxOrderInj {α : Type u_1} [BEq α] [ReflBEq α] {xs ys : List α} (h : xs.Sublist ys) : Fin xs.length → Fin ys.length

Sublist.idxOrderInj is an order-preserving injective map from Fin xs.length to Fin ys.length which exists when we have xs <+ ys: conceptually it represents an order-preserving embedding of one list into the other. For example:

(by decide : [0, 1, 1] <+ [5, 0, 1, 3, 1]).idxInj 1 = 2

Equations

• h.idxOrderInj = ⋯.idxInj

@[simp]

theorem List.Sublist.subperm_idxOrderInj {α : Type u_1} [BEq α] [ReflBEq α] {xs ys : List α} (h : xs.Sublist ys) : ⋯.idxInj = h.idxOrderInj

@[simp]

theorem List.Sublist.coe_idxOrderInj {α : Type u_1} [BEq α] [ReflBEq α] {xs ys : List α} (h : xs.Sublist ys) {i : Fin xs.length} : ↑(h.idxOrderInj i) = idxOfNth xs[i] ys (countBefore xs[i] xs ↑i)

theorem List.Sublist.getElem_idxOrderInj_eq_getElem {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} (h : xs.Sublist ys) {i : Fin xs.length} : ys[↑(h.idxOrderInj i)] = xs[↑i]

theorem List.Sublist.idxOrderInj_injective {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} (h : xs.Sublist ys) : Function.Injective h.idxOrderInj

@[simp]

theorem List.Sublist.idxOrderInj_inj {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} {h : xs.Sublist ys} (i j : Fin xs.length) : h.idxOrderInj i = h.idxOrderInj j ↔ i = j

def List.Perm.idxBij {α : Type u_1} [BEq α] [ReflBEq α] {xs ys : List α} (h : xs.Perm ys) : Fin xs.length → Fin ys.length

Perm.idxBij is a bijective map from Fin xs.length to Fin ys.length which exists when we have xs.Perm ys: conceptually it represents a permuting of one list into the other. For example:

(by decide : [0, 1, 1, 3, 5] ~ [5, 0, 1, 3, 1]).idxBij 2 = 4

Equations

• h.idxBij = ⋯.idxInj

@[simp]

theorem List.Perm.subperm_idxBij {α : Type u_1} [BEq α] [ReflBEq α] {xs ys : List α} (h : xs.Perm ys) : ⋯.idxInj = h.idxBij

@[simp]

theorem List.Perm.coe_idxBij {α : Type u_1} [BEq α] [ReflBEq α] {xs ys : List α} (h : xs.Perm ys) {i : Fin xs.length} : ↑(h.idxBij i) = idxOfNth xs[i] ys (countBefore xs[i] xs ↑i)

theorem List.Perm.getElem_idxBij_eq_getElem {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} (hxy : xs.Perm ys) (i : Fin xs.length) : ys[↑(hxy.idxBij i)] = xs[↑i]

theorem List.Perm.getElem_idxBij_symm_eq_getElem {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} (hxy : xs.Perm ys) (i : Fin ys.length) : xs[↑(⋯.idxBij i)] = ys[↑i]

theorem List.Perm.idxBij_leftInverse_idxBij_symm {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} (h : xs.Perm ys) : Function.LeftInverse h.idxBij ⋯.idxBij

theorem List.Perm.idxBij_rightInverse_idxBij_symm {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} (h : xs.Perm ys) : Function.RightInverse h.idxBij ⋯.idxBij

theorem List.Perm.idxBij_symm_rightInverse_idxBij {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} (h : xs.Perm ys) : Function.RightInverse ⋯.idxBij h.idxBij

theorem List.Perm.idxBij_symm_leftInverse_idxBij {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} (h : xs.Perm ys) : Function.LeftInverse ⋯.idxBij h.idxBij

theorem List.Perm.idxBij_idxBij_symm {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} (h : xs.Perm ys) {i : Fin ys.length} : h.idxBij (⋯.idxBij i) = i

theorem List.Perm.idxBij_symm_idxBij {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} (h : xs.Perm ys) {i : Fin xs.length} : ⋯.idxBij (h.idxBij i) = i

theorem List.Perm.idxBij_injective {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} (h : xs.Perm ys) : Function.Injective h.idxBij

theorem List.Perm.idxBij_surjective {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} (h : xs.Perm ys) : Function.Surjective h.idxBij