List Permutations #
This file introduces the List.Perm
relation, which is true if two lists are permutations of one
another.
Notation #
The notation ~
is used for permutation equivalence.
theorem
List.Perm.subperm_left
{α : Type u_1}
{l l₁ l₂ : List α}
(p : l₁.Perm l₂)
:
l.Subperm l₁ ↔ l.Subperm l₂
theorem
List.Perm.subperm_right
{α : Type u_1}
{l₁ l₂ l : List α}
(p : l₁.Perm l₂)
:
l₁.Subperm l ↔ l₂.Subperm l
theorem
List.Subperm.trans
{α : Type u_1}
{l₁ l₂ l₃ : List α}
(s₁₂ : l₁.Subperm l₂)
(s₂₃ : l₂.Subperm l₃)
:
l₁.Subperm l₃
theorem
List.Subperm.cons_right
{α : Type u_1}
{l l' : List α}
(x : α)
(h : l.Subperm l')
:
l.Subperm (x :: l')
theorem
List.Subperm.length_le
{α : Type u_1}
{l₁ l₂ : List α}
:
l₁.Subperm l₂ → l₁.length ≤ l₂.length
theorem
List.Subperm.perm_of_length_le
{α : Type u_1}
{l₁ l₂ : List α}
:
l₁.Subperm l₂ → l₂.length ≤ l₁.length → l₁.Perm l₂
theorem
List.Subperm.antisymm
{α : Type u_1}
{l₁ l₂ : List α}
(h₁ : l₁.Subperm l₂)
(h₂ : l₂.Subperm l₁)
:
l₁.Perm l₂
theorem
List.Subperm.filter
{α : Type u_1}
(p : α → Bool)
⦃l l' : List α⦄
(h : l.Subperm l')
:
(List.filter p l).Subperm (List.filter p l')
theorem
List.Subperm.countP_le
{α : Type u_1}
(p : α → Bool)
{l₁ l₂ : List α}
:
l₁.Subperm l₂ → List.countP p l₁ ≤ List.countP p l₂
theorem
List.Subperm.count_le
{α : Type u_1}
[DecidableEq α]
{l₁ l₂ : List α}
(s : l₁.Subperm l₂)
(a : α)
:
List.count a l₁ ≤ List.count a l₂
theorem
List.cons_subperm_of_not_mem_of_mem
{α : Type u_1}
{a : α}
{l₁ l₂ : List α}
(h₁ : ¬a ∈ l₁)
(h₂ : a ∈ l₂)
(s : l₁.Subperm l₂)
:
(a :: l₁).Subperm l₂
Weaker version of Subperm.cons_left
theorem
List.subperm_of_subset
{α✝ : Type u_1}
{l₁ l₂ : List α✝}
(d : l₁.Nodup)
(H : l₁ ⊆ l₂)
:
l₁.Subperm l₂
theorem
List.subperm_cons_erase
{α : Type u_1}
[DecidableEq α]
(a : α)
(l : List α)
:
l.Subperm (a :: l.erase a)
theorem
List.erase_subperm
{α : Type u_1}
[DecidableEq α]
(a : α)
(l : List α)
:
(l.erase a).Subperm l
theorem
List.Subperm.erase
{α : Type u_1}
[DecidableEq α]
{l₁ l₂ : List α}
(a : α)
(h : l₁.Subperm l₂)
:
(l₁.erase a).Subperm (l₂.erase a)
theorem
List.Perm.diff_right
{α : Type u_1}
[DecidableEq α]
{l₁ l₂ : List α}
(t : List α)
(h : l₁.Perm l₂)
:
(l₁.diff t).Perm (l₂.diff t)
theorem
List.Perm.diff_left
{α : Type u_1}
[DecidableEq α]
(l : List α)
{t₁ t₂ : List α}
(h : t₁.Perm t₂)
:
l.diff t₁ = l.diff t₂
theorem
List.Perm.diff
{α : Type u_1}
[DecidableEq α]
{l₁ l₂ t₁ t₂ : List α}
(hl : l₁.Perm l₂)
(ht : t₁.Perm t₂)
:
(l₁.diff t₁).Perm (l₂.diff t₂)
theorem
List.Subperm.diff_right
{α : Type u_1}
[DecidableEq α]
{l₁ l₂ : List α}
(h : l₁.Subperm l₂)
(t : List α)
:
(l₁.diff t).Subperm (l₂.diff t)
theorem
List.subperm_append_diff_self_of_count_le
{α : Type u_1}
[DecidableEq α]
{l₁ l₂ : List α}
(h : ∀ (x : α), x ∈ l₁ → List.count x l₁ ≤ List.count x l₂)
:
(l₁ ++ l₂.diff l₁).Perm l₂
The list version of add_tsub_cancel_of_le
for multisets.
theorem
List.subperm_ext_iff
{α : Type u_1}
[DecidableEq α]
{l₁ l₂ : List α}
:
l₁.Subperm l₂ ↔ ∀ (x : α), x ∈ l₁ → List.count x l₁ ≤ List.count x l₂
The list version of Multiset.le_iff_count
.
instance
List.decidableSubperm
{α : Type u_1}
[DecidableEq α]
:
DecidableRel fun (x1 x2 : List α) => x1.Subperm x2
Equations
- x✝¹.decidableSubperm x✝ = decidable_of_iff (x✝¹.isSubperm x✝ = true) ⋯
theorem
List.Subperm.cons_left
{α : Type u_1}
[DecidableEq α]
{l₁ l₂ : List α}
(h : l₁.Subperm l₂)
(x : α)
(hx : List.count x l₁ < List.count x l₂)
:
(x :: l₁).Subperm l₂
theorem
List.perm_insertIdx
{α : Type u_1}
(x : α)
(l : List α)
{n : Nat}
(h : n ≤ l.length)
:
(List.insertIdx n x l).Perm (x :: l)
@[deprecated List.perm_insertIdx]
theorem
List.perm_insertNth
{α : Type u_1}
(x : α)
(l : List α)
{n : Nat}
(h : n ≤ l.length)
:
(List.insertIdx n x l).Perm (x :: l)
Alias of List.perm_insertIdx
.
theorem
List.Perm.union_right
{α : Type u_1}
[DecidableEq α]
{l₁ l₂ : List α}
(t₁ : List α)
(h : l₁.Perm l₂)
:
theorem
List.Perm.union_left
{α : Type u_1}
[DecidableEq α]
(l : List α)
{t₁ t₂ : List α}
(h : t₁.Perm t₂)
:
theorem
List.Perm.union
{α : Type u_1}
[DecidableEq α]
{l₁ l₂ t₁ t₂ : List α}
(p₁ : l₁.Perm l₂)
(p₂ : t₁.Perm t₂)
:
theorem
List.Perm.inter_left
{α : Type u_1}
[DecidableEq α]
(l : List α)
{t₁ t₂ : List α}
(p : t₁.Perm t₂)
:
theorem
List.Perm.inter
{α : Type u_1}
[DecidableEq α]
{l₁ l₂ t₁ t₂ : List α}
(p₁ : l₁.Perm l₂)
(p₂ : t₁.Perm t₂)
:
theorem
List.Perm.flatten_congr
{α : Type u_1}
{l₁ l₂ : List (List α)}
:
List.Forall₂ (fun (x1 x2 : List α) => x1.Perm x2) l₁ l₂ → l₁.flatten.Perm l₂.flatten
@[deprecated List.Perm.flatten_congr]
theorem
List.Perm.join_congr
{α : Type u_1}
{l₁ l₂ : List (List α)}
:
List.Forall₂ (fun (x1 x2 : List α) => x1.Perm x2) l₁ l₂ → l₁.flatten.Perm l₂.flatten
Alias of List.Perm.flatten_congr
.
theorem
List.perm_insertP
{α : Type u_1}
(p : α → Bool)
(a : α)
(l : List α)
:
(List.insertP p a l).Perm (a :: l)
theorem
List.Perm.insertP
{α : Type u_1}
{l₁ l₂ : List α}
(p : α → Bool)
(a : α)
(h : l₁.Perm l₂)
:
(List.insertP p a l₁).Perm (List.insertP p a l₂)
theorem
List.Perm.merge
{α : Type u_1}
{l₁ l₂ r₁ r₂ : List α}
(s₁ s₂ : α → α → Bool)
(hl : l₁.Perm l₂)
(hr : r₁.Perm r₂)
:
(l₁.merge r₁ s₁).Perm (l₂.merge r₂ s₂)