Mathlib.Data.List.Perm.Subperm

List.subperm_iff_count theorem

[DecidableEq α] : l₁ <+~ l₂ ↔ ∀ a, count a l₁ ≤ count a l₂

Full source

/-- See also `List.subperm_ext_iff`. -/
lemma subperm_iff_count [DecidableEq α] : l₁ <+~ l₂l₁ <+~ l₂ ↔ ∀ a, count a l₁ ≤ count a l₂ :=
  subperm_ext_iff.trans <| forall_congr' fun a ↦ by
    by_cases ha : a ∈ l₁ <;> simp [ha, count_eq_zero_of_not_mem]

Sub-permutation Criterion via Element Counts

Informal description

For any two lists $l₁$ and $l₂$ over a type $\alpha$ with decidable equality, $l₁$ is a sub-permutation of $l₂$ (denoted $l₁ <+~ l₂$) if and only if for every element $a$ in $\alpha$, the count of $a$ in $l₁$ is less than or equal to its count in $l₂$.

List.subperm_iff theorem

: l₁ <+~ l₂ ↔ ∃ l, l ~ l₂ ∧ l₁ <+ l

Full source

lemma subperm_iff : l₁ <+~ l₂l₁ <+~ l₂ ↔ ∃ l, l ~ l₂ ∧ l₁ <+ l := by
  refine ⟨?_, fun ⟨l, h₁, h₂⟩ ↦ h₂.subperm.trans h₁.subperm⟩
  rintro ⟨l, h₁, h₂⟩
  obtain ⟨l', h₂⟩ := h₂.exists_perm_append
  exact ⟨l₁ ++ l', (h₂.trans (h₁.append_right _)).symm, (prefix_append _ _).sublist⟩

Sub-permutation Characterization via Permutation and Sublist

Informal description

For any two lists $l_1$ and $l_2$, $l_1$ is a sub-permutation of $l_2$ (denoted $l_1 <+~ l_2$) if and only if there exists a list $l$ that is a permutation of $l_2$ and $l_1$ is a sublist of $l$.

List.subperm_singleton_iff theorem

: l <+~ [a] ↔ l = [] ∨ l = [a]

Full source

@[simp] lemma subperm_singleton_iff : l <+~ [a]l <+~ [a] ↔ l = [] ∨ l = [a] := by
  constructor
  · rw [subperm_iff]
    rintro ⟨s, hla, h⟩
    rwa [perm_singleton.mp hla, sublist_singleton] at h
  · rintro (rfl | rfl)
    exacts [nil_subperm, Subperm.refl _]

Sub-permutation Criterion for Singleton Lists: $l <+~ [a] \leftrightarrow l = [] \lor l = [a]$

Informal description

For any list $l$ and element $a$, $l$ is a sub-permutation of the singleton list $[a]$ (denoted $l <+~ [a]$) if and only if $l$ is the empty list or $l$ is the singleton list $[a]$.

List.subperm_cons_self theorem

: l <+~ a :: l

Full source

lemma subperm_cons_self : l <+~ a :: l := ⟨l, Perm.refl _, sublist_cons_self _ _⟩

List is Sub-permutation of Its Extension by Any Element

Informal description

For any list $l$ and element $a$, the list $l$ is a sub-permutation of the list obtained by prepending $a$ to $l$, i.e., $l \prec a :: l$.

List.cons_subperm_of_mem theorem

 {a : α} {l₁ l₂ : List α} (_ : Nodup l₁) (h₁ : a ∉ l₁) (h₂ : a ∈ l₂) (s : l₁ <+~ l₂) : a :: l₁ <+~ l₂

Full source

@[deprecated List.cons_subperm_of_not_mem_of_mem (since := "2024-12-11"), nolint unusedArguments]
theorem cons_subperm_of_mem {a : α} {l₁ l₂ : List α} (_ : Nodup l₁) (h₁ : a ∉ l₁) (h₂ : a ∈ l₂)
    (s : l₁ <+~ l₂) : a :: l₁a :: l₁ <+~ l₂ :=
  cons_subperm_of_not_mem_of_mem h₁ h₂ s

Sub-permutation Preservation under Cons with Unique Element

Informal description

Let $l_1$ and $l_2$ be lists of elements of type $\alpha$, and let $a$ be an element of $\alpha$. If: 1. $l_1$ has no duplicate elements, 2. $a$ does not belong to $l_1$, 3. $a$ belongs to $l_2$, and 4. $l_1$ is a sub-permutation of $l_2$, then the list obtained by prepending $a$ to $l_1$ is also a sub-permutation of $l_2$.

List.Nodup.subperm theorem

(d : Nodup l₁) (H : l₁ ⊆ l₂) : l₁ <+~ l₂

Full source

protected theorem Nodup.subperm (d : Nodup l₁) (H : l₁ ⊆ l₂) : l₁ <+~ l₂ :=
  subperm_of_subset d H

Existence of Sub-permutation for Nodup Lists under Inclusion

Informal description

For any list $l_1$ with no duplicate elements and any list $l_2$ such that every element of $l_1$ is contained in $l_2$, there exists a sub-permutation of $l_2$ that is equal to $l_1$.

Notation