List Sub-permutations #

This file develops theory about the List.Subperm relation.

Notation #

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

theorem List.subperm_iff_count {α : Type u_1} {l₁ l₂ : List α} [DecidableEq α] :

l₁.Subperm l₂ ↔ ∀ (a : α), List.count a l₁ ≤ List.count a l₂

theorem List.subperm_iff {α : Type u_1} {l₁ l₂ : List α} :

l₁.Subperm l₂ ↔ ∃ (l : List α), l.Perm l₂ ∧ l₁.Sublist l

@[simp]

theorem List.subperm_singleton_iff {α : Type u_1} {l : List α} {a : α} :

l.Subperm [a] ↔ l = [] ∨ l = [a]

theorem List.subperm_cons_self {α : Type u_1} {l : List α} {a : α} :

l.Subperm (a :: l)

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.

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.

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

(a :: l₁).Subperm l₂

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

l₁.Subperm l₂