List Permutations

This file develops theory about the List.Perm relation.

Notation

The notation ~ is used for permutation equivalence.

instance List.instTransPerm_mathlib {α : Type u_1} : Trans List.Perm List.Perm List.Perm

Equations

• List.instTransPerm_mathlib = { trans := ⋯ }

theorem List.perm_rfl {α : Type u_1} {l : List α} : l.Perm l

theorem List.Perm.subset_congr_left {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₃ : List α} (h : l₁.Perm l₂) : l₁ ⊆ l₃ ↔ l₂ ⊆ l₃

theorem List.Perm.subset_congr_right {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₃ : List α} (h : l₁.Perm l₂) : l₃ ⊆ l₁ ↔ l₃ ⊆ l₂

theorem List.perm_comp_perm {α : Type u_1} : Relation.Comp List.Perm List.Perm = List.Perm

theorem List.perm_comp_forall₂ {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {l : List α} {u : List α} {v : List β} (hlu : l.Perm u) (huv : List.Forall₂ r u v) : Relation.Comp (List.Forall₂ r) List.Perm l v

theorem List.forall₂_comp_perm_eq_perm_comp_forall₂ {α : Type u_1} {β : Type u_2} {r : α → β → Prop} : Relation.Comp (List.Forall₂ r) List.Perm = Relation.Comp List.Perm (List.Forall₂ r)

theorem List.rel_perm_imp {α : Type u_1} {β : Type u_2} {r : α → β → Prop} (hr : Relator.RightUnique r) : (List.Forall₂ r ⇒ List.Forall₂ r ⇒ fun (x1 x2 : Prop) => x1 → x2) List.Perm List.Perm

theorem List.rel_perm {α : Type u_1} {β : Type u_2} {r : α → β → Prop} (hr : Relator.BiUnique r) : (List.Forall₂ r ⇒ List.Forall₂ r ⇒ fun (x1 x2 : Prop) => x1 ↔ x2) List.Perm List.Perm

theorem List.subperm_iff {α : Type u_1} {l₁ : List α} {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_cons_self {α : Type u_1} {l : List α} {a : α} : l.Subperm (a :: l)

theorem List.count_eq_count_filter_add {α : Type u_1} [DecidableEq α] (P : α → Prop) [DecidablePred P] (l : List α) (a : α) : List.count a l = List.count a (List.filter (fun (b : α) => decide (P b)) l) + List.count a (List.filter (fun (x : α) => decide ¬P x) l)

theorem List.Perm.foldl_eq {α : Type u_1} {β : Type u_2} {f : β → α → β} {l₁ : List α} {l₂ : List α} [rcomm : RightCommutative f] (p : l₁.Perm l₂) (b : β) : List.foldl f b l₁ = List.foldl f b l₂

theorem List.Perm.foldr_eq {α : Type u_1} {β : Type u_2} {f : α → β → β} {l₁ : List α} {l₂ : List α} [lcomm : LeftCommutative f] (p : l₁.Perm l₂) (b : β) : List.foldr f b l₁ = List.foldr f b l₂

theorem List.Perm.foldl_op_eq {α : Type u_1} {op : α → α → α} [IA : Std.Associative op] [IC : Std.Commutative op] {l₁ : List α} {l₂ : List α} {a : α} (h : l₁.Perm l₂) : List.foldl op a l₁ = List.foldl op a l₂

theorem List.Perm.foldr_op_eq {α : Type u_1} {op : α → α → α} [IA : Std.Associative op] [IC : Std.Commutative op] {l₁ : List α} {l₂ : List α} {a : α} (h : l₁.Perm l₂) : List.foldr op a l₁ = List.foldr op a l₂

@[deprecated List.Perm.foldl_op_eq]

theorem List.Perm.fold_op_eq {α : Type u_1} {op : α → α → α} [IA : Std.Associative op] [IC : Std.Commutative op] {l₁ : List α} {l₂ : List α} {a : α} (h : l₁.Perm l₂) : List.foldl op a l₁ = List.foldl op a l₂

Alias of List.Perm.foldl_op_eq.

theorem List.perm_option_toList {α : Type u_1} {o₁ : Option α} {o₂ : Option α} : o₁.toList.Perm o₂.toList ↔ o₁ = o₂

@[deprecated List.perm_option_toList]

theorem List.perm_option_to_list {α : Type u_1} {o₁ : Option α} {o₂ : Option α} : o₁.toList.Perm o₂.toList ↔ o₁ = o₂

Alias of List.perm_option_toList.

theorem List.subperm.cons {α : Type u_1} (a : α) {l₁ : List α} {l₂ : List α} : l₁.Subperm l₂ → (a :: l₁).Subperm (a :: l₂)

Alias of the reverse direction of List.subperm_cons.

theorem List.subperm.of_cons {α : Type u_1} (a : α) {l₁ : List α} {l₂ : List α} : (a :: l₁).Subperm (a :: l₂) → l₁.Subperm l₂

Alias of the forward direction of List.subperm_cons.

theorem List.cons_subperm_of_mem {α : Type u_1} {a : α} {l₁ : List α} {l₂ : List α} (d₁ : l₁.Nodup) (h₁ : a ∉ l₁) (h₂ : a ∈ l₂) (s : l₁.Subperm l₂) : (a :: l₁).Subperm l₂

theorem List.Nodup.subperm {α : Type u_1} {l₁ : List α} {l₂ : List α} (d : l₁.Nodup) (H : l₁ ⊆ l₂) : l₁.Subperm l₂

theorem List.Perm.bagInter_right {α : Type u_1} [DecidableEq α] {l₁ : List α} {l₂ : List α} (t : List α) (h : l₁.Perm l₂) : (l₁.bagInter t).Perm (l₂.bagInter t)

theorem List.Perm.bagInter_left {α : Type u_1} [DecidableEq α] (l : List α) {t₁ : List α} {t₂ : List α} (p : t₁.Perm t₂) : l.bagInter t₁ = l.bagInter t₂

theorem List.Perm.bagInter {α : Type u_1} [DecidableEq α] {l₁ : List α} {l₂ : List α} {t₁ : List α} {t₂ : List α} (hl : l₁.Perm l₂) (ht : t₁.Perm t₂) : (l₁.bagInter t₁).Perm (l₂.bagInter t₂)

theorem List.perm_replicate_append_replicate {α : Type u_1} [DecidableEq α] {l : List α} {a : α} {b : α} {m : ℕ} {n : ℕ} (h : a ≠ b) : l.Perm (List.replicate m a ++ List.replicate n b) ↔ List.count a l = m ∧ List.count b l = n ∧ l ⊆ [a, b]

theorem List.Perm.dedup {α : Type u_1} [DecidableEq α] {l₁ : List α} {l₂ : List α} (p : l₁.Perm l₂) : l₁.dedup.Perm l₂.dedup

theorem List.Perm.inter_append {α : Type u_1} [DecidableEq α] {l : List α} {t₁ : List α} {t₂ : List α} (h : t₁.Disjoint t₂) : (l ∩ (t₁ ++ t₂)).Perm (l ∩ t₁ ++ l ∩ t₂)

theorem List.Perm.bind_left {α : Type u_1} {β : Type u_2} (l : List α) {f : α → List β} {g : α → List β} (h : ∀ a ∈ l, (f a).Perm (g a)) : (l.bind f).Perm (l.bind g)

theorem List.bind_append_perm {α : Type u_1} {β : Type u_2} (l : List α) (f : α → List β) (g : α → List β) : (l.bind f ++ l.bind g).Perm (l.bind fun (x : α) => f x ++ g x)

theorem List.map_append_bind_perm {α : Type u_1} {β : Type u_2} (l : List α) (f : α → β) (g : α → List β) : (List.map f l ++ l.bind g).Perm (l.bind fun (x : α) => f x :: g x)

theorem List.Perm.product_right {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List α} (t₁ : List β) (p : l₁.Perm l₂) : (l₁.product t₁).Perm (l₂.product t₁)

theorem List.Perm.product_left {α : Type u_1} {β : Type u_2} (l : List α) {t₁ : List β} {t₂ : List β} (p : t₁.Perm t₂) : (l.product t₁).Perm (l.product t₂)

theorem List.Perm.product {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List α} {t₁ : List β} {t₂ : List β} (p₁ : l₁.Perm l₂) (p₂ : t₁.Perm t₂) : (l₁.product t₁).Perm (l₂.product t₂)

theorem List.perm_lookmap {α : Type u_1} (f : α → Option α) {l₁ : List α} {l₂ : List α} (H : List.Pairwise (fun (a b : α) => ∀ c ∈ f a, ∀ d ∈ f b, a = b ∧ c = d) l₁) (p : l₁.Perm l₂) : (List.lookmap f l₁).Perm (List.lookmap f l₂)

theorem List.Perm.take_inter {α : Type u_1} [DecidableEq α] {xs : List α} {ys : List α} (n : ℕ) (h : xs.Perm ys) (h' : ys.Nodup) : (List.take n xs).Perm (ys.inter (List.take n xs))

theorem List.Perm.drop_inter {α : Type u_1} [DecidableEq α] {xs : List α} {ys : List α} (n : ℕ) (h : xs.Perm ys) (h' : ys.Nodup) : (List.drop n xs).Perm (ys.inter (List.drop n xs))

theorem List.Perm.dropSlice_inter {α : Type u_1} [DecidableEq α] {xs : List α} {ys : List α} (n : ℕ) (m : ℕ) (h : xs.Perm ys) (h' : ys.Nodup) : (List.dropSlice n m xs).Perm (ys ∩ List.dropSlice n m xs)