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.instTransListPerm = { trans := ⋯ }
theorem
List.perm_comp_forall₂
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
{l : List α}
{u : List α}
{v : List β}
(hlu : List.Perm l 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.subperm_iff
{α : Type u_1}
{l₁ : List α}
{l₂ : List α}
:
List.Subperm l₁ l₂ ↔ ∃ (l : List α), List.Perm l l₂ ∧ List.Sublist l₁ l
@[simp]
theorem
List.subperm_singleton_iff
{α : Type u_1}
{l : List α}
{a : α}
:
List.Subperm l [a] ↔ l = [] ∨ l = [a]
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 : List.Perm l₁ 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 : List.Perm l₁ 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 : List.Perm l₁ l₂)
:
List.foldl op a l₁ = List.foldl op a l₂
theorem
List.perm_option_to_list
{α : Type u_1}
{o₁ : Option α}
{o₂ : Option α}
:
List.Perm (Option.toList o₁) (Option.toList o₂) ↔ o₁ = o₂
theorem
List.subperm.of_cons
{α : Type u_1}
(a : α)
{l₁ : List α}
{l₂ : List α}
:
List.Subperm (a :: l₁) (a :: l₂) → List.Subperm l₁ l₂
Alias of the forward direction of List.subperm_cons.
theorem
List.subperm.cons
{α : Type u_1}
(a : α)
{l₁ : List α}
{l₂ : List α}
:
List.Subperm l₁ l₂ → List.Subperm (a :: l₁) (a :: l₂)
Alias of the reverse direction of List.subperm_cons.
theorem
List.cons_subperm_of_mem
{α : Type u_1}
{a : α}
{l₁ : List α}
{l₂ : List α}
(d₁ : List.Nodup l₁)
(h₁ : a ∉ l₁)
(h₂ : a ∈ l₂)
(s : List.Subperm l₁ l₂)
:
List.Subperm (a :: l₁) l₂
theorem
List.Nodup.subperm
{α : Type u_1}
{l₁ : List α}
{l₂ : List α}
(d : List.Nodup l₁)
(H : l₁ ⊆ l₂)
:
List.Subperm l₁ l₂
theorem
List.Perm.bagInter_right
{α : Type u_1}
[DecidableEq α]
{l₁ : List α}
{l₂ : List α}
(t : List α)
(h : List.Perm l₁ l₂)
:
List.Perm (List.bagInter l₁ t) (List.bagInter l₂ t)
theorem
List.Perm.bagInter_left
{α : Type u_1}
[DecidableEq α]
(l : List α)
{t₁ : List α}
{t₂ : List α}
(p : List.Perm t₁ t₂)
:
List.bagInter l t₁ = List.bagInter l t₂
theorem
List.Perm.bagInter
{α : Type u_1}
[DecidableEq α]
{l₁ : List α}
{l₂ : List α}
{t₁ : List α}
{t₂ : List α}
(hl : List.Perm l₁ l₂)
(ht : List.Perm t₁ t₂)
:
List.Perm (List.bagInter l₁ t₁) (List.bagInter l₂ t₂)
theorem
List.perm_replicate_append_replicate
{α : Type u_1}
[DecidableEq α]
{l : List α}
{a : α}
{b : α}
{m : ℕ}
{n : ℕ}
(h : a ≠ b)
:
List.Perm l (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 : List.Perm l₁ l₂)
:
List.Perm (List.dedup l₁) (List.dedup l₂)
theorem
List.Perm.inter_append
{α : Type u_1}
[DecidableEq α]
{l : List α}
{t₁ : List α}
{t₂ : List α}
(h : List.Disjoint t₁ t₂)
:
theorem
List.Perm.product_right
{α : Type u_1}
{β : Type u_2}
{l₁ : List α}
{l₂ : List α}
(t₁ : List β)
(p : List.Perm l₁ l₂)
:
List.Perm (List.product l₁ t₁) (List.product l₂ t₁)
theorem
List.Perm.product_left
{α : Type u_1}
{β : Type u_2}
(l : List α)
{t₁ : List β}
{t₂ : List β}
(p : List.Perm t₁ t₂)
:
List.Perm (List.product l t₁) (List.product l t₂)
theorem
List.Perm.product
{α : Type u_1}
{β : Type u_2}
{l₁ : List α}
{l₂ : List α}
{t₁ : List β}
{t₂ : List β}
(p₁ : List.Perm l₁ l₂)
(p₂ : List.Perm t₁ t₂)
:
List.Perm (List.product l₁ t₁) (List.product l₂ 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 : List.Perm l₁ l₂)
:
List.Perm (List.lookmap f l₁) (List.lookmap f l₂)
theorem
List.Perm.take_inter
{α : Type u_3}
[DecidableEq α]
{xs : List α}
{ys : List α}
(n : ℕ)
(h : List.Perm xs ys)
(h' : List.Nodup ys)
:
List.Perm (List.take n xs) (List.inter ys (List.take n xs))
theorem
List.Perm.drop_inter
{α : Type u_3}
[DecidableEq α]
{xs : List α}
{ys : List α}
(n : ℕ)
(h : List.Perm xs ys)
(h' : List.Nodup ys)
:
List.Perm (List.drop n xs) (List.inter ys (List.drop n xs))
theorem
List.Perm.dropSlice_inter
{α : Type u_3}
[DecidableEq α]
{xs : List α}
{ys : List α}
(n : ℕ)
(m : ℕ)
(h : List.Perm xs ys)
(h' : List.Nodup ys)
:
List.Perm (List.dropSlice n m xs) (ys ∩ List.dropSlice n m xs)
theorem
List.perm_of_mem_permutationsAux
{α : Type u_1}
{ts : List α}
{is : List α}
{l : List α}
:
l ∈ List.permutationsAux ts is → List.Perm l (ts ++ is)
theorem
List.perm_of_mem_permutations
{α : Type u_1}
{l₁ : List α}
{l₂ : List α}
(h : l₁ ∈ List.permutations l₂)
:
List.Perm l₁ l₂
theorem
List.length_permutationsAux
{α : Type u_1}
(ts : List α)
(is : List α)
:
List.length (List.permutationsAux ts is) + Nat.factorial (List.length is) = Nat.factorial (List.length ts + List.length is)
@[simp]
theorem
List.mem_permutations
{α : Type u_1}
{s : List α}
{t : List α}
:
s ∈ List.permutations t ↔ List.Perm s t
theorem
List.perm_permutations'Aux_comm
{α : Type u_1}
(a : α)
(b : α)
(l : List α)
:
List.Perm (List.bind (List.permutations'Aux a l) (List.permutations'Aux b))
(List.bind (List.permutations'Aux b l) (List.permutations'Aux a))
theorem
List.permutations_perm_permutations'
{α : Type u_1}
(ts : List α)
:
List.Perm (List.permutations ts) (List.permutations' ts)
@[simp]
theorem
List.mem_permutations'
{α : Type u_1}
{s : List α}
{t : List α}
:
s ∈ List.permutations' t ↔ List.Perm s t
@[simp]
theorem
List.perm_permutations_iff
{α : Type u_1}
{s : List α}
{t : List α}
:
List.Perm (List.permutations s) (List.permutations t) ↔ List.Perm s t
@[simp]
theorem
List.perm_permutations'_iff
{α : Type u_1}
{s : List α}
{t : List α}
:
List.Perm (List.permutations' s) (List.permutations' t) ↔ List.Perm s t
theorem
List.nthLe_permutations'Aux
{α : Type u_1}
(s : List α)
(x : α)
(n : ℕ)
(hn : n < List.length (List.permutations'Aux x s))
:
List.nthLe (List.permutations'Aux x s) 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.length (List.takeWhile (fun (x_1 : α) => decide (x = x_1)) l) + 1
@[simp]
theorem
List.length_permutations'Aux
{α : Type u_1}
(s : List α)
(x : α)
:
List.length (List.permutations'Aux x s) = List.length s + 1
@[simp]
theorem
List.permutations'Aux_nthLe_zero
{α : Type u_1}
(s : List α)
(x : α)
(hn : optParam (0 < List.length (List.permutations'Aux x s)) ⋯)
:
List.nthLe (List.permutations'Aux x s) 0 hn = x :: s
theorem
List.nodup_permutations'Aux_iff
{α : Type u_1}
{s : List α}
{x : α}
:
List.Nodup (List.permutations'Aux x s) ↔ x ∉ s