# List Sub-permutations #

This file develops theory about the `List.Subperm` relation.

## Notation #

The notation `<+~` is used for sub-permutations.

source
theorem List.subperm_iff_count {α : Type u_1} {l₁ l₂ : List α} [DecidableEq α] :
l₁.Subperm l₂ ↔ ∀ (a : α), count a l₁ ≤ count a l₂

See also `List.subperm_ext_iff`.

source
theorem List.subperm_iff {α : Type u_1} {l₁ l₂ : List α} :
l₁.Subperm l₂ ↔ ∃ (l : List α), l.Perm l₂ ∧ l₁.Sublist l
source
@[simp]
theorem List.subperm_singleton_iff {α : Type u_1} {l : List α} {a : α} :
l.Subperm [a] ↔ l = [] ∨ l = [a]
source
theorem List.subperm_cons_self {α : Type u_1} {l : List α} {a : α} :
l.Subperm (a :: l)
source
theorem List.subperm.cons {α : Type u_1} (a : α) {l₁ l₂ : List α} :
l₁.Subperm l₂ → (a :: l₁).Subperm (a :: l₂)

Alias of the reverse direction of `List.subperm_cons`.

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

Alias of the forward direction of `List.subperm_cons`.

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