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.
Equations
- List.instTransPerm_mathlib = { trans := ⋯ }
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 (x x_1 : Prop) => x → x_1) 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 (x x_1 : Prop) => x ↔ x_1) List.Perm List.Perm
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.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 the forward direction of List.subperm_cons.
Alias of the reverse direction of List.subperm_cons.
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_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)
:
theorem
List.Perm.drop_inter
{α : Type u_1}
[DecidableEq α]
{xs : List α}
{ys : List α}
(n : ℕ)
(h : xs.Perm ys)
(h' : ys.Nodup)
:
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)
theorem
List.length_permutations
{α : Type u_1}
(l : List α)
:
l.permutations.length = l.length.factorial
theorem
List.perm_permutations'Aux_comm
{α : Type u_1}
(a : α)
(b : α)
(l : List α)
:
((List.permutations'Aux a l).bind (List.permutations'Aux b)).Perm
((List.permutations'Aux b l).bind (List.permutations'Aux a))
theorem
List.Perm.permutations'
{α : Type u_1}
{s : List α}
{t : List α}
(p : s.Perm t)
:
s.permutations'.Perm t.permutations'
theorem
List.permutations_perm_permutations'
{α : Type u_1}
(ts : List α)
:
ts.permutations.Perm ts.permutations'
theorem
List.Perm.permutations
{α : Type u_1}
{s : List α}
{t : List α}
(h : s.Perm t)
:
s.permutations.Perm t.permutations
theorem
List.get_permutations'Aux
{α : Type u_1}
(s : List α)
(x : α)
(n : ℕ)
(hn : n < (List.permutations'Aux x s).length)
:
(List.permutations'Aux x s).get ⟨n, hn⟩ = List.insertNth n x s
@[deprecated List.get_permutations'Aux]
theorem
List.nthLe_permutations'Aux
{α : Type u_1}
(s : List α)
(x : α)
(n : ℕ)
(hn : n < (List.permutations'Aux x s).length)
:
(List.permutations'Aux x s).nthLe n hn = List.insertNth n x s
theorem
List.count_permutations'Aux_self
{α : Type u_1}
[DecidableEq α]
(l : List α)
(x : α)
:
List.count (x :: l) (List.permutations'Aux x l) = (List.takeWhile (fun (x_1 : α) => decide (x = x_1)) l).length + 1
@[simp]
theorem
List.length_permutations'Aux
{α : Type u_1}
(s : List α)
(x : α)
:
(List.permutations'Aux x s).length = s.length + 1
@[simp]
theorem
List.permutations'Aux_get_zero
{α : Type u_1}
(s : List α)
(x : α)
(hn : optParam (0 < (List.permutations'Aux x s).length) ⋯)
:
(List.permutations'Aux x s).get ⟨0, hn⟩ = x :: s
theorem
List.nodup_permutations'Aux_of_not_mem
{α : Type u_1}
(s : List α)
(x : α)
(hx : x ∉ s)
:
(List.permutations'Aux x s).Nodup
theorem
List.nodup_permutations'Aux_iff
{α : Type u_1}
{s : List α}
{x : α}
:
(List.permutations'Aux x s).Nodup ↔ x ∉ s