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.

theorem List.Subperm.append {α : Type u_1} {l₁ l₂ r₁ r₂ : List α} : l₁.Subperm l₂ → r₁.Subperm r₂ → (l₁ ++ r₁).Subperm (l₂ ++ r₂)

theorem List.map_subperm_map_iff {α : Type u_2} {β : Type u_3} {l₁ l₂ : List α} {f : α → β} (hf : Function.Injective f) : (map f l₁).Subperm (map f l₂) ↔ l₁.Subperm l₂

theorem List.Subperm.map {α : Type u_2} {β : Type u_3} {l₁ l₂ : List α} {f : α → β} (hf : Function.Injective f) : l₁.Subperm l₂ → (List.map f l₁).Subperm (List.map f l₂)

Alias of the reverse direction of List.map_subperm_map_iff.

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