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 : α), count a l₁ ≤ count a l₂

See also List.subperm_ext_iff.

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.

@[deprecated List.cons_subperm_of_not_mem_of_mem (since := "2024-12-11")]

theorem List.cons_subperm_of_mem {α : Type u_1} {a : α} {l₁ l₂ : List α} : 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₂