List Permutations

This file develops theory about the List.Perm relation.

Notation

The notation ~ is used for permutation equivalence.

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

instance List.instIsEquivPerm {α : Type u_1} : IsEquiv (List α) Perm

instance List.instIsPreorderSubperm {α : Type u_1} : IsPreorder (List α) Subperm

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

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

theorem List.set_perm_cons_eraseIdx {α : Type u_1} {l : List α} {n : ℕ} (h : n < l.length) (a : α) : (l.set n a).Perm (a :: l.eraseIdx n)

theorem List.getElem_cons_eraseIdx_perm {α : Type u_1} {l : List α} {n : ℕ} (h : n < l.length) : (l[n] :: l.eraseIdx n).Perm l

theorem List.perm_insertIdx_iff_of_le {α : Type u_1} {l₁ l₂ : List α} {m n : ℕ} (hm : m ≤ l₁.length) (hn : n ≤ l₂.length) (a : α) : (l₁.insertIdx m a).Perm (l₂.insertIdx n a) ↔ l₁.Perm l₂

theorem List.Perm.insertIdx_of_le {α : Type u_1} {l₁ l₂ : List α} {m n : ℕ} (hm : m ≤ l₁.length) (hn : n ≤ l₂.length) (a : α) : l₁.Perm l₂ → (l₁.insertIdx m a).Perm (l₂.insertIdx n a)

Alias of the reverse direction of List.perm_insertIdx_iff_of_le.

@[simp]

theorem List.perm_insertIdx_iff {α : Type u_1} {l₁ l₂ : List α} {n : ℕ} {a : α} : (l₁.insertIdx n a).Perm (l₂.insertIdx n a) ↔ l₁.Perm l₂

theorem List.Perm.insertIdx {α : Type u_1} {l₁ l₂ : List α} (h : l₁.Perm l₂) (n : ℕ) (a : α) : (l₁.insertIdx n a).Perm (l₂.insertIdx n a)

theorem List.perm_eraseIdx_of_getElem?_eq {α : Type u_1} {l₁ l₂ : List α} {m n : ℕ} (h : l₁[m]? = l₂[n]?) : (l₁.eraseIdx m).Perm (l₂.eraseIdx n) ↔ l₁.Perm l₂

theorem List.Perm.eraseIdx_of_getElem?_eq {α : Type u_1} {l₁ l₂ : List α} {m n : ℕ} (h : l₁[m]? = l₂[n]?) : l₁.Perm l₂ → (l₁.eraseIdx m).Perm (l₂.eraseIdx n)

Alias of the reverse direction of List.perm_eraseIdx_of_getElem?_eq.

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

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

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

theorem List.eq_map_comp_perm {α : Type u_1} {β : Type u_2} (f : α → β) : (Relation.Comp (fun (x1 : List β) (x2 : List α) => x1 = map f x2) fun (x1 x2 : List α) => x1.Perm x2) = fun (x1 : List β) (x2 : List α) => x1.Perm (map f x2)

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

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

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

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

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

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

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

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

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

theorem List.map_perm_map_iff {α : Type u_1} {β : Type u_2} {l l' : List α} {f : α → β} (hf : Function.Injective f) : (map f l).Perm (map f l') ↔ l.Perm l'

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

theorem List.Perm.flatMap {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α} {f g : α → List β} (h : l₁.Perm l₂) (hfg : ∀ (a : α), a ∈ l₁ → (f a).Perm (g a)) : (flatMap f l₁).Perm (flatMap g l₂)

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

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

theorem List.Perm.product_right {α : Type u_1} {β : Type u_2} {l₁ 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₁ t₂ : List β} (p : t₁.Perm t₂) : (l.product t₁).Perm (l.product t₂)

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