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.Sublist.subperm
{α : Type u_1}
{l₁ : List α}
{l₂ : List α}
(s : l₁.Sublist l₂)
:
l₁.Subperm l₂
theorem
List.Perm.subperm
{α : Type u_1}
{l₁ : List α}
{l₂ : List α}
(p : l₁.Perm l₂)
:
l₁.Subperm l₂
theorem
List.Subperm.antisymm
{α : Type u_1}
{l₁ : List α}
{l₂ : List α}
(h₁ : l₁.Subperm l₂)
(h₂ : l₂.Subperm l₁)
:
l₁.Perm l₂
theorem
List.Subperm.filter
{α : Type u_1}
(p : α → Bool)
⦃l : List α⦄
⦃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₁ : List α}
{l₂ : List α}
:
l₁.Subperm l₂ → List.countP p l₁ ≤ List.countP p l₂
theorem
List.Subperm.count_le
{α : Type u_1}
[DecidableEq α]
{l₁ : List α}
{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₁ : List α}
{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_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₁ : List α}
{l₂ : List α}
(a : α)
(h : l₁.Subperm l₂)
:
(l₁.erase a).Subperm (l₂.erase a)
theorem
List.Perm.diff_right
{α : Type u_1}
[DecidableEq α]
{l₁ : List α}
{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₁ : List α}
{t₂ : List α}
(h : t₁.Perm t₂)
:
l.diff t₁ = l.diff t₂
theorem
List.Perm.diff
{α : Type u_1}
[DecidableEq α]
{l₁ : List α}
{l₂ : List α}
{t₁ : List α}
{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₁ : List α}
{l₂ : List α}
(h : l₁.Subperm l₂)
(t : List α)
:
(l₁.diff t).Subperm (l₂.diff t)
theorem
List.erase_cons_subperm_cons_erase
{α : Type u_1}
[DecidableEq α]
(a : α)
(b : α)
(l : List α)
:
theorem
List.subperm_append_diff_self_of_count_le
{α : Type u_1}
[DecidableEq α]
{l₁ : List α}
{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₁ : List α}
{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₁ : List α}
{l₂ : List α}
(h : l₁.Subperm l₂)
(x : α)
(hx : List.count x l₁ < List.count x l₂)
:
(x :: l₁).Subperm l₂
theorem
List.perm_insertNth
{α : Type u_1}
(x : α)
(l : List α)
{n : Nat}
(h : n ≤ l.length)
:
(List.insertNth n x l).Perm (x :: l)
theorem
List.Perm.union_right
{α : Type u_1}
[DecidableEq α]
{l₁ : List α}
{l₂ : List α}
(t₁ : List α)
(h : l₁.Perm l₂)
:
theorem
List.Perm.union_left
{α : Type u_1}
[DecidableEq α]
(l : List α)
{t₁ : List α}
{t₂ : List α}
(h : t₁.Perm t₂)
:
theorem
List.Perm.union
{α : Type u_1}
[DecidableEq α]
{l₁ : List α}
{l₂ : List α}
{t₁ : List α}
{t₂ : List α}
(p₁ : l₁.Perm l₂)
(p₂ : t₁.Perm t₂)
:
theorem
List.Perm.inter_right
{α : Type u_1}
[DecidableEq α]
{l₁ : List α}
{l₂ : List α}
(t₁ : List α)
:
theorem
List.Perm.inter_left
{α : Type u_1}
[DecidableEq α]
(l : List α)
{t₁ : List α}
{t₂ : List α}
(p : t₁.Perm t₂)
:
theorem
List.Perm.inter
{α : Type u_1}
[DecidableEq α]
{l₁ : List α}
{l₂ : List α}
{t₁ : List α}
{t₂ : List α}
(p₁ : l₁.Perm l₂)
(p₂ : t₁.Perm t₂)
:
theorem
List.Perm.join_congr
{α : Type u_1}
{l₁ : List (List α)}
{l₂ : List (List α)}
:
List.Forall₂ (fun (x1 x2 : List α) => x1.Perm x2) l₁ l₂ → l₁.join.Perm l₂.join
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₁ : List α}
{l₂ : List α}
(p : α → Bool)
(a : α)
(h : l₁.Perm l₂)
:
(List.insertP p a l₁).Perm (List.insertP p a l₂)