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.

@[simp]

theorem List.Perm.refl {α : Type u_1} (l : List α) : List.Perm l l

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

theorem List.Perm.of_eq : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ = l₂ → List.Perm l₁ l₂

theorem List.Perm.symm {α : Type u_1} {l₁ : List α} {l₂ : List α} (h : List.Perm l₁ l₂) : List.Perm l₂ l₁

theorem List.perm_comm {α : Type u_1} {l₁ : List α} {l₂ : List α} : List.Perm l₁ l₂ ↔ List.Perm l₂ l₁

theorem List.Perm.swap' {α : Type u_1} (x : α) (y : α) {l₁ : List α} {l₂ : List α} (p : List.Perm l₁ l₂) : List.Perm (y :: x :: l₁) (x :: y :: l₂)

theorem List.Perm.recOnSwap' {α : Type u_1} {motive : (l₁ l₂ : List α) → List.Perm l₁ l₂ → Prop} {l₁ : List α} {l₂ : List α} (p : List.Perm l₁ l₂) (nil : motive [] [] (_ : List.Perm [] [])) (cons : ∀ (x : α) {l₁ l₂ : List α} (h : List.Perm l₁ l₂), motive l₁ l₂ h → motive (x :: l₁) (x :: l₂) (_ : List.Perm (x :: l₁) (x :: l₂))) (swap' : ∀ (x y : α) {l₁ l₂ : List α} (h : List.Perm l₁ l₂), motive l₁ l₂ h → motive (y :: x :: l₁) (x :: y :: l₂) (_ : List.Perm (y :: x :: l₁) (x :: y :: l₂))) (trans : ∀ {l₁ l₂ l₃ : List α} (h₁ : List.Perm l₁ l₂) (h₂ : List.Perm l₂ l₃), motive l₁ l₂ h₁ → motive l₂ l₃ h₂ → motive l₁ l₃ (_ : List.Perm l₁ l₃)) : motive l₁ l₂ p

Similar to Perm.recOn, but the swap case is generalized to Perm.swap', where the tail of the lists are not necessarily the same.

theorem List.Perm.eqv (α : Type u_1) : Equivalence List.Perm

instance List.isSetoid (α : Type u_1) : Setoid (List α)

Equations

• List.isSetoid α = { r := List.Perm, iseqv := (_ : Equivalence List.Perm) }

theorem List.Perm.mem_iff {α : Type u_1} {a : α} {l₁ : List α} {l₂ : List α} (p : List.Perm l₁ l₂) : a ∈ l₁ ↔ a ∈ l₂

theorem List.Perm.subset {α : Type u_1} {l₁ : List α} {l₂ : List α} (p : List.Perm l₁ l₂) : l₁ ⊆ l₂

theorem List.Perm.append_right {α : Type u_1} {l₁ : List α} {l₂ : List α} (t₁ : List α) (p : List.Perm l₁ l₂) : List.Perm (l₁ ++ t₁) (l₂ ++ t₁)

theorem List.Perm.append_left {α : Type u_1} {t₁ : List α} {t₂ : List α} (l : List α) : List.Perm t₁ t₂ → List.Perm (l ++ t₁) (l ++ t₂)

theorem List.Perm.append {α : Type u_1} {l₁ : List α} {l₂ : List α} {t₁ : List α} {t₂ : List α} (p₁ : List.Perm l₁ l₂) (p₂ : List.Perm t₁ t₂) : List.Perm (l₁ ++ t₁) (l₂ ++ t₂)

theorem List.Perm.append_cons {α : Type u_1} (a : α) {h₁ : List α} {h₂ : List α} {t₁ : List α} {t₂ : List α} (p₁ : List.Perm h₁ h₂) (p₂ : List.Perm t₁ t₂) : List.Perm (h₁ ++ a :: t₁) (h₂ ++ a :: t₂)

@[simp]

theorem List.perm_middle {α : Type u_1} {a : α} {l₁ : List α} {l₂ : List α} : List.Perm (l₁ ++ a :: l₂) (a :: (l₁ ++ l₂))

@[simp]

theorem List.perm_append_singleton {α : Type u_1} (a : α) (l : List α) : List.Perm (l ++ [a]) (a :: l)

theorem List.perm_append_comm {α : Type u_1} {l₁ : List α} {l₂ : List α} : List.Perm (l₁ ++ l₂) (l₂ ++ l₁)

theorem List.concat_perm {α : Type u_1} (l : List α) (a : α) : List.Perm (List.concat l a) (a :: l)

theorem List.Perm.length_eq {α : Type u_1} {l₁ : List α} {l₂ : List α} (p : List.Perm l₁ l₂) : List.length l₁ = List.length l₂

theorem List.Perm.eq_nil {α : Type u_1} {l : List α} (p : List.Perm l []) : l = []

theorem List.Perm.nil_eq {α : Type u_1} {l : List α} (p : List.Perm [] l) : [] = l

@[simp]

theorem List.perm_nil {α : Type u_1} {l₁ : List α} : List.Perm l₁ [] ↔ l₁ = []

@[simp]

theorem List.nil_perm {α : Type u_1} {l₁ : List α} : List.Perm [] l₁ ↔ l₁ = []

theorem List.not_perm_nil_cons {α : Type u_1} (x : α) (l : List α) : ¬List.Perm [] (x :: l)

@[simp]

theorem List.reverse_perm {α : Type u_1} (l : List α) : List.Perm (List.reverse l) l

theorem List.perm_cons_append_cons {α : Type u_1} {l : List α} {l₁ : List α} {l₂ : List α} (a : α) (p : List.Perm l (l₁ ++ l₂)) : List.Perm (a :: l) (l₁ ++ a :: l₂)

@[simp]

theorem List.perm_replicate {α : Type u_1} {n : Nat} {a : α} {l : List α} : List.Perm l (List.replicate n a) ↔ l = List.replicate n a

@[simp]

theorem List.replicate_perm {α : Type u_1} {n : Nat} {a : α} {l : List α} : List.Perm (List.replicate n a) l ↔ List.replicate n a = l

@[simp]

theorem List.perm_singleton {α : Type u_1} {a : α} {l : List α} : List.Perm l [a] ↔ l = [a]

@[simp]

theorem List.singleton_perm {α : Type u_1} {a : α} {l : List α} : List.Perm [a] l ↔ [a] = l

theorem List.Perm.eq_singleton {α : Type u_1} {a : α} {l : List α} : List.Perm l [a] → l = [a]

Alias of the forward direction of List.perm_singleton.

theorem List.Perm.singleton_eq {α : Type u_1} {a : α} {l : List α} : List.Perm [a] l → [a] = l

Alias of the forward direction of List.singleton_perm.

theorem List.singleton_perm_singleton {α : Type u_1} {a : α} {b : α} : List.Perm [a] [b] ↔ a = b

theorem List.perm_cons_erase {α : Type u_1} [DecidableEq α] {a : α} {l : List α} (h : a ∈ l) : List.Perm l (a :: List.erase l a)

theorem List.Perm.filterMap {α : Type u_1} {β : Type u_2} (f : α → Option β) {l₁ : List α} {l₂ : List α} (p : List.Perm l₁ l₂) : List.Perm (List.filterMap f l₁) (List.filterMap f l₂)

theorem List.Perm.map {α : Type u_1} {β : Type u_2} (f : α → β) {l₁ : List α} {l₂ : List α} (p : List.Perm l₁ l₂) : List.Perm (List.map f l₁) (List.map f l₂)

theorem List.Perm.pmap {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : (a : α) → p✝ a → β) {l₁ : List α} {l₂ : List α} (p : List.Perm l₁ l₂) {H₁ : ∀ (a : α), a ∈ l₁ → p✝ a} {H₂ : ∀ (a : α), a ∈ l₂ → p✝ a} : List.Perm (List.pmap f l₁ H₁) (List.pmap f l₂ H₂)

theorem List.Perm.filter {α : Type u_1} (p : α → Bool) {l₁ : List α} {l₂ : List α} (s : List.Perm l₁ l₂) : List.Perm (List.filter p l₁) (List.filter p l₂)

theorem List.filter_append_perm {α : Type u_1} (p : α → Bool) (l : List α) : List.Perm (List.filter p l ++ List.filter (fun (x : α) => !p x) l) l

theorem List.exists_perm_sublist {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₂' : List α} (s : List.Sublist l₁ l₂) (p : List.Perm l₂ l₂') : ∃ (l₁' : List α), List.Perm l₁' l₁ ∧ List.Sublist l₁' l₂'

theorem List.Perm.sizeOf_eq_sizeOf {α : Type u_1} [SizeOf α] {l₁ : List α} {l₂ : List α} (h : List.Perm l₁ l₂) : sizeOf l₁ = sizeOf l₂

theorem List.nil_subperm {α : Type u_1} {l : List α} : List.Subperm [] l

theorem List.Perm.subperm_left {α : Type u_1} {l : List α} {l₁ : List α} {l₂ : List α} (p : List.Perm l₁ l₂) : List.Subperm l l₁ ↔ List.Subperm l l₂

theorem List.Perm.subperm_right {α : Type u_1} {l₁ : List α} {l₂ : List α} {l : List α} (p : List.Perm l₁ l₂) : List.Subperm l₁ l ↔ List.Subperm l₂ l

theorem List.Sublist.subperm {α : Type u_1} {l₁ : List α} {l₂ : List α} (s : List.Sublist l₁ l₂) : List.Subperm l₁ l₂

theorem List.Perm.subperm {α : Type u_1} {l₁ : List α} {l₂ : List α} (p : List.Perm l₁ l₂) : List.Subperm l₁ l₂

theorem List.Subperm.refl {α : Type u_1} (l : List α) : List.Subperm l l

theorem List.Subperm.trans {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₃ : List α} (s₁₂ : List.Subperm l₁ l₂) (s₂₃ : List.Subperm l₂ l₃) : List.Subperm l₁ l₃

theorem List.Subperm.cons_right {α : Type u_1} {l : List α} {l' : List α} (x : α) (h : List.Subperm l l') : List.Subperm l (x :: l')

theorem List.Subperm.length_le {α : Type u_1} {l₁ : List α} {l₂ : List α} : List.Subperm l₁ l₂ → List.length l₁ ≤ List.length l₂

theorem List.Subperm.perm_of_length_le {α : Type u_1} {l₁ : List α} {l₂ : List α} : List.Subperm l₁ l₂ → List.length l₂ ≤ List.length l₁ → List.Perm l₁ l₂

theorem List.Subperm.antisymm {α : Type u_1} {l₁ : List α} {l₂ : List α} (h₁ : List.Subperm l₁ l₂) (h₂ : List.Subperm l₂ l₁) : List.Perm l₁ l₂

theorem List.Subperm.subset {α : Type u_1} {l₁ : List α} {l₂ : List α} : List.Subperm l₁ l₂ → l₁ ⊆ l₂

theorem List.Subperm.filter {α : Type u_1} (p : α → Bool) ⦃l : List α⦄ ⦃l' : List α⦄ (h : List.Subperm l l') : List.Subperm (List.filter p l) (List.filter p l')

@[simp]

theorem List.singleton_subperm_iff {α : Type u_1} {l : List α} {a : α} : List.Subperm [a] l ↔ a ∈ l

theorem List.Sublist.exists_perm_append {α : Type u_1} {l₁ : List α} {l₂ : List α} : List.Sublist l₁ l₂ → ∃ (l : List α), List.Perm l₂ (l₁ ++ l)

theorem List.Perm.countP_eq {α : Type u_1} (p : α → Bool) {l₁ : List α} {l₂ : List α} (s : List.Perm l₁ l₂) : List.countP p l₁ = List.countP p l₂

theorem List.Subperm.countP_le {α : Type u_1} (p : α → Bool) {l₁ : List α} {l₂ : List α} : List.Subperm l₁ l₂ → List.countP p l₁ ≤ List.countP p l₂

theorem List.Perm.countP_congr {α : Type u_1} {l₁ : List α} {l₂ : List α} (s : List.Perm l₁ l₂) {p : α → Bool} {p' : α → Bool} (hp : ∀ (x : α), x ∈ l₁ → p x = p' x) : List.countP p l₁ = List.countP p' l₂

theorem List.countP_eq_countP_filter_add {α : Type u_1} (l : List α) (p : α → Bool) (q : α → Bool) : List.countP p l = List.countP p (List.filter q l) + List.countP p (List.filter (fun (a : α) => !q a) l)

theorem List.Perm.count_eq {α : Type u_1} [DecidableEq α] {l₁ : List α} {l₂ : List α} (p : List.Perm l₁ l₂) (a : α) : List.count a l₁ = List.count a l₂

theorem List.Subperm.count_le {α : Type u_1} [DecidableEq α] {l₁ : List α} {l₂ : List α} (s : List.Subperm l₁ l₂) (a : α) : List.count a l₁ ≤ List.count a l₂

theorem List.Perm.foldl_eq' {β : Type u_1} {α : Type u_2} {f : β → α → β} {l₁ : List α} {l₂ : List α} (p : List.Perm l₁ l₂) (comm : ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₁ → ∀ (z : β), f (f z x) y = f (f z y) x) (init : β) : List.foldl f init l₁ = List.foldl f init l₂

theorem List.Perm.rec_heq {α : Type u_1} {β : List α → Sort u_2} {f : (a : α) → (l : List α) → β l → β (a :: l)} {b : β []} {l : List α} {l' : List α} (hl : List.Perm l l') (f_congr : ∀ {a : α} {l l' : List α} {b : β l} {b' : β l'}, List.Perm l l' → HEq b b' → HEq (f a l b) (f a l' b')) (f_swap : ∀ {a a' : α} {l : List α} {b : β l}, HEq (f a (a' :: l) (f a' l b)) (f a' (a :: l) (f a l b))) : HEq (List.rec b f l) (List.rec b f l')

theorem List.perm_inv_core {α : Type u_1} {a : α} {l₁ : List α} {l₂ : List α} {r₁ : List α} {r₂ : List α} : List.Perm (l₁ ++ a :: r₁) (l₂ ++ a :: r₂) → List.Perm (l₁ ++ r₁) (l₂ ++ r₂)

Lemma used to destruct perms element by element.

theorem List.Perm.cons_inv {α : Type u_1} {a : α} {l₁ : List α} {l₂ : List α} : List.Perm (a :: l₁) (a :: l₂) → List.Perm l₁ l₂

@[simp]

theorem List.perm_cons {α : Type u_1} (a : α) {l₁ : List α} {l₂ : List α} : List.Perm (a :: l₁) (a :: l₂) ↔ List.Perm l₁ l₂

theorem List.perm_append_left_iff {α : Type u_1} {l₁ : List α} {l₂ : List α} (l : List α) : List.Perm (l ++ l₁) (l ++ l₂) ↔ List.Perm l₁ l₂

theorem List.perm_append_right_iff {α : Type u_1} {l₁ : List α} {l₂ : List α} (l : List α) : List.Perm (l₁ ++ l) (l₂ ++ l) ↔ List.Perm l₁ l₂

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

Weaker version of Subperm.cons_left

theorem List.subperm_append_left {α : Type u_1} {l₁ : List α} {l₂ : List α} (l : List α) : List.Subperm (l ++ l₁) (l ++ l₂) ↔ List.Subperm l₁ l₂

theorem List.subperm_append_right {α : Type u_1} {l₁ : List α} {l₂ : List α} (l : List α) : List.Subperm (l₁ ++ l) (l₂ ++ l) ↔ List.Subperm l₁ l₂

theorem List.Subperm.exists_of_length_lt {α : Type u_1} {l₁ : List α} {l₂ : List α} (s : List.Subperm l₁ l₂) (h : List.length l₁ < List.length l₂) : ∃ (a : α), List.Subperm (a :: l₁) l₂

theorem List.subperm_of_subset : ∀ {α : Type u_1} {l₁ l₂ : List α}, List.Nodup l₁ → l₁ ⊆ l₂ → List.Subperm l₁ l₂

theorem List.perm_ext_iff_of_nodup {α : Type u_1} {l₁ : List α} {l₂ : List α} (d₁ : List.Nodup l₁) (d₂ : List.Nodup l₂) : List.Perm l₁ l₂ ↔ ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂

theorem List.Nodup.perm_iff_eq_of_sublist {α : Type u_1} {l₁ : List α} {l₂ : List α} {l : List α} (d : List.Nodup l) (s₁ : List.Sublist l₁ l) (s₂ : List.Sublist l₂ l) : List.Perm l₁ l₂ ↔ l₁ = l₂

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

theorem List.subperm_cons_erase {α : Type u_1} [DecidableEq α] (a : α) (l : List α) : List.Subperm l (a :: List.erase l a)

theorem List.erase_subperm {α : Type u_1} [DecidableEq α] (a : α) (l : List α) : List.Subperm (List.erase l a) l

theorem List.Subperm.erase {α : Type u_1} [DecidableEq α] {l₁ : List α} {l₂ : List α} (a : α) (h : List.Subperm l₁ l₂) : List.Subperm (List.erase l₁ a) (List.erase l₂ a)

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

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

theorem List.Perm.diff {α : 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.diff l₁ t₁) (List.diff l₂ t₂)

theorem List.Subperm.diff_right {α : Type u_1} [DecidableEq α] {l₁ : List α} {l₂ : List α} (h : List.Subperm l₁ l₂) (t : List α) : List.Subperm (List.diff l₁ t) (List.diff l₂ t)

theorem List.erase_cons_subperm_cons_erase {α : Type u_1} [DecidableEq α] (a : α) (b : α) (l : List α) : List.Subperm (List.erase (a :: l) b) (a :: List.erase l b)

theorem List.subperm_cons_diff {α : Type u_1} [DecidableEq α] {a : α} {l₁ : List α} {l₂ : List α} : List.Subperm (List.diff (a :: l₁) l₂) (a :: List.diff l₁ l₂)

theorem List.subset_cons_diff {α : Type u_1} [DecidableEq α] {a : α} {l₁ : List α} {l₂ : List α} : List.diff (a :: l₁) l₂ ⊆ a :: List.diff l₁ l₂

theorem List.cons_perm_iff_perm_erase {α : Type u_1} [DecidableEq α] {a : α} {l₁ : List α} {l₂ : List α} : List.Perm (a :: l₁) l₂ ↔ a ∈ l₂ ∧ List.Perm l₁ (List.erase l₂ a)

theorem List.perm_iff_count {α : Type u_1} [DecidableEq α] {l₁ : List α} {l₂ : List α} : List.Perm l₁ l₂ ↔ ∀ (a : α), List.count a l₁ = List.count a 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₂) : List.Perm (l₁ ++ List.diff l₂ l₁) 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 α} : List.Subperm l₁ 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 α} : List.isSubperm l₁ l₂ = true ↔ List.Subperm l₁ l₂

instance List.decidableSubperm {α : Type u_1} [DecidableEq α] : DecidableRel fun (x x_1 : List α) => List.Subperm x x_1

Equations

• List.decidableSubperm x✝ x = decidable_of_iff (List.isSubperm x✝ x = true) (_ : List.isSubperm x✝ x = true ↔ List.Subperm x✝ x)

theorem List.Subperm.cons_left {α : Type u_1} [DecidableEq α] {l₁ : List α} {l₂ : List α} (h : List.Subperm l₁ l₂) (x : α) (hx : List.count x l₁ < List.count x l₂) : List.Subperm (x :: l₁) l₂

theorem List.isPerm_iff {α : Type u_1} [DecidableEq α] {l₁ : List α} {l₂ : List α} : List.isPerm l₁ l₂ = true ↔ List.Perm l₁ l₂

instance List.decidablePerm {α : Type u_1} [DecidableEq α] (l₁ : List α) (l₂ : List α) : Decidable (List.Perm l₁ l₂)

Equations

• List.decidablePerm l₁ l₂ = decidable_of_iff (List.isPerm l₁ l₂ = true) (_ : List.isPerm l₁ l₂ = true ↔ List.Perm l₁ l₂)

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

theorem List.perm_insert_swap {α : Type u_1} [DecidableEq α] (x : α) (y : α) (l : List α) : List.Perm (List.insert x (List.insert y l)) (List.insert y (List.insert x l))

theorem List.perm_insertNth {α : Type u_1} (x : α) (l : List α) {n : Nat} (h : n ≤ List.length l) : List.Perm (List.insertNth n x l) (x :: l)

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

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

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

theorem List.Perm.inter_right {α : Type u_1} [DecidableEq α] {l₁ : List α} {l₂ : List α} (t₁ : List α) : List.Perm l₁ l₂ → List.Perm (l₁ ∩ t₁) (l₂ ∩ t₁)

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

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

theorem List.Perm.pairwise_iff {α : Type u_1} {R : α → α → Prop} (S : ∀ {x y : α}, R x y → R y x) {l₁ : List α} {l₂ : List α} (_p : List.Perm l₁ l₂) : List.Pairwise R l₁ ↔ List.Pairwise R l₂

theorem List.Pairwise.perm {α : Type u_1} {R : α → α → Prop} {l : List α} {l' : List α} (hR : List.Pairwise R l) (hl : List.Perm l l') (hsymm : ∀ {x y : α}, R x y → R y x) : List.Pairwise R l'

theorem List.Perm.pairwise {α : Type u_1} {R : α → α → Prop} {l : List α} {l' : List α} (hl : List.Perm l l') (hR : List.Pairwise R l) (hsymm : ∀ {x y : α}, R x y → R y x) : List.Pairwise R l'

theorem List.Perm.nodup_iff {α : Type u_1} {l₁ : List α} {l₂ : List α} : List.Perm l₁ l₂ → (List.Nodup l₁ ↔ List.Nodup l₂)

theorem List.Perm.join {α : Type u_1} {l₁ : List (List α)} {l₂ : List (List α)} (h : List.Perm l₁ l₂) : List.Perm (List.join l₁) (List.join l₂)

theorem List.Perm.bind_right {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List α} (f : α → List β) (p : List.Perm l₁ l₂) : List.Perm (List.bind l₁ f) (List.bind l₂ f)

theorem List.Perm.join_congr {α : Type u_1} {l₁ : List (List α)} {l₂ : List (List α)} : List.Forall₂ (fun (x x_1 : List α) => List.Perm x x_1) l₁ l₂ → List.Perm (List.join l₁) (List.join l₂)

theorem List.Perm.eraseP {α : Type u_1} (f : α → Bool) {l₁ : List α} {l₂ : List α} (H : List.Pairwise (fun (a b : α) => f a = true → f b = true → False) l₁) (p : List.Perm l₁ l₂) : List.Perm (List.eraseP f l₁) (List.eraseP f l₂)