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.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.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.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₂