Documentation

Batteries.Data.List.Perm

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.nil_subperm {α : Type u_1} {l : List α} :
[].Subperm l
theorem List.Perm.subperm_left {α : Type u_1} {l : List α} {l₁ : List α} {l₂ : List α} (p : l₁.Perm l₂) :
l.Subperm l₁ l.Subperm l₂
theorem List.Perm.subperm_right {α : Type u_1} {l₁ : List α} {l₂ : List α} {l : List α} (p : l₁.Perm l₂) :
l₁.Subperm l l₂.Subperm l
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.refl {α : Type u_1} (l : List α) :
l.Subperm l
theorem List.Subperm.trans {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₃ : List α} (s₁₂ : l₁.Subperm l₂) (s₂₃ : l₂.Subperm l₃) :
l₁.Subperm l₃
theorem List.Subperm.cons_right {α : Type u_1} {l : List α} {l' : List α} (x : α) (h : l.Subperm l') :
l.Subperm (x :: l')
theorem List.Subperm.length_le {α : Type u_1} {l₁ : List α} {l₂ : List α} :
l₁.Subperm l₂l₁.length l₂.length
theorem List.Subperm.perm_of_length_le {α : Type u_1} {l₁ : List α} {l₂ : List α} :
l₁.Subperm l₂l₂.length l₁.lengthl₁.Perm 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.subset {α : Type u_1} {l₁ : List α} {l₂ : List α} :
l₁.Subperm l₂l₁ 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')
@[simp]
theorem List.singleton_subperm_iff {α : Type u_1} {l : List α} {a : α} :
[a].Subperm l a 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.subperm_cons {α : Type u_1} (a : α) {l₁ : List α} {l₂ : List α} :
(a :: l₁).Subperm (a :: l₂) l₁.Subperm 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_append_left {α : Type u_1} {l₁ : List α} {l₂ : List α} (l : List α) :
(l ++ l₁).Subperm (l ++ l₂) l₁.Subperm l₂
theorem List.subperm_append_right {α : Type u_1} {l₁ : List α} {l₂ : List α} (l : List α) :
(l₁ ++ l).Subperm (l₂ ++ l) l₁.Subperm l₂
theorem List.Subperm.exists_of_length_lt {α : Type u_1} {l₁ : List α} {l₂ : List α} (s : l₁.Subperm l₂) (h : l₁.length < l₂.length) :
∃ (a : α), (a :: l₁).Subperm l₂
theorem List.subperm_of_subset :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Nodupl₁ l₂l₁.Subperm l₂
theorem List.perm_ext_iff_of_nodup {α : Type u_1} {l₁ : List α} {l₂ : List α} (d₁ : l₁.Nodup) (d₂ : l₂.Nodup) :
l₁.Perm l₂ ∀ (a : α), a l₁ a l₂
theorem List.Nodup.perm_iff_eq_of_sublist {α : Type u_1} {l₁ : List α} {l₂ : List α} {l : List α} (d : l.Nodup) (s₁ : l₁.Sublist l) (s₂ : l₂.Sublist l) :
l₁.Perm l₂ l₁ = 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₁ : 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 α) :
((a :: l).erase b).Subperm (a :: l.erase b)
theorem List.subperm_cons_diff {α : Type u_1} [DecidableEq α] {a : α} {l₁ : List α} {l₂ : List α} :
((a :: l₁).diff l₂).Subperm (a :: l₁.diff l₂)
theorem List.subset_cons_diff {α : Type u_1} [DecidableEq α] {a : α} {l₁ : List α} {l₂ : List α} :
(a :: l₁).diff l₂ a :: l₁.diff l₂
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.

theorem List.isSubperm_iff {α : Type u_1} [DecidableEq α] {l₁ : List α} {l₂ : List α} :
l₁.isSubperm l₂ = true l₁.Subperm l₂
instance List.decidableSubperm {α : Type u_1} [DecidableEq α] :
DecidableRel fun (x1 x2 : List α) => x1.Subperm x2
Equations
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₂) :
(l₁ t₁).Perm (l₂ t₁)
theorem List.Perm.union_left {α : Type u_1} [DecidableEq α] (l : List α) {t₁ : List α} {t₂ : List α} (h : t₁.Perm t₂) :
(l t₁).Perm (l 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₂) :
(l₁ t₁).Perm (l₂ t₂)
theorem List.Perm.inter_right {α : Type u_1} [DecidableEq α] {l₁ : List α} {l₂ : List α} (t₁ : List α) :
l₁.Perm l₂(l₁ t₁).Perm (l₂ t₁)
theorem List.Perm.inter_left {α : Type u_1} [DecidableEq α] (l : List α) {t₁ : List α} {t₂ : List α} (p : t₁.Perm t₂) :
l t₁ = l 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₂) :
(l₁ t₁).Perm (l₂ 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₂)
@[irreducible]
theorem List.perm_merge {α : Type u_1} (s : ααBool) (l : List α) (r : List α) :
(l.merge r s).Perm (l ++ r)
theorem List.Perm.merge {α : Type u_1} {l₁ : List α} {l₂ : List α} {r₁ : List α} {r₂ : List α} (s₁ : ααBool) (s₂ : ααBool) (hl : l₁.Perm l₂) (hr : r₁.Perm r₂) :
(l₁.merge r₁ s₁).Perm (l₂.merge r₂ s₂)