# Lemmas about `List.Pairwise` and `List.Nodup`. #

## Pairwise and Nodup #

### Pairwise #

source
theorem List.Pairwise.sublist {α✝ : Type u_1} {l₁ l₂ : List α✝} {R : α✝ → α✝ → Prop} :
l₁.Sublist l₂ → Pairwise R l₂ → Pairwise R l₁
source
theorem List.Pairwise.imp {α : Type u_1} {R S : α → α → Prop} (H : ∀ {a b : α}, R a b → S a b) {l : List α} :
Pairwise R l → Pairwise S l
source
theorem List.rel_of_pairwise_cons {α✝ : Type u_1} {a : α✝} {l : List α✝} {R : α✝ → α✝ → Prop} (p : Pairwise R (a :: l)) {a' : α✝} :
a' ∈ l → R a a'
source
theorem List.Pairwise.of_cons {α✝ : Type u_1} {a : α✝} {l : List α✝} {R : α✝ → α✝ → Prop} (p : Pairwise R (a :: l)) :
Pairwise R l
source
theorem List.Pairwise.tail {α : Type u_1} {R : α → α → Prop} {l : List α} (h : Pairwise R l) :
Pairwise R l.tail
source
theorem List.Pairwise.imp_of_mem {α : Type u_1} {l : List α} {R S : α → α → Prop} (H : ∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) (p : Pairwise R l) :
Pairwise S l
source
theorem List.Pairwise.and {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {l : List α✝} {S : α✝ → α✝ → Prop} (hR : Pairwise R l) (hS : Pairwise S l) :
Pairwise (fun (a b : α✝) => R a b ∧ S a b) l
source
theorem List.pairwise_and_iff {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {l : List α✝} {S : α✝ → α✝ → Prop} :
Pairwise (fun (a b : α✝) => R a b ∧ S a b) l ↔ Pairwise R l ∧ Pairwise S l
source
theorem List.Pairwise.imp₂ {α✝ : Type u_1} {R S T : α✝ → α✝ → Prop} {l : List α✝} (H : ∀ (a b : α✝), R a b → S a b → T a b) (hR : Pairwise R l) (hS : Pairwise S l) :
Pairwise T l
source
theorem List.Pairwise.iff_of_mem {α : Type u_1} {R S : α → α → Prop} {l : List α} (H : ∀ {a b : α}, a ∈ l → b ∈ l → (R a b ↔ S a b)) :
Pairwise R l ↔ Pairwise S l
source
theorem List.Pairwise.iff {α : Type u_1} {R S : α → α → Prop} (H : ∀ (a b : α), R a b ↔ S a b) {l : List α} :
Pairwise R l ↔ Pairwise S l
source
theorem List.pairwise_of_forall {α : Type u_1} {R : α → α → Prop} {l : List α} (H : ∀ (x y : α), R x y) :
Pairwise R l
source
theorem List.Pairwise.and_mem {α : Type u_1} {R : α → α → Prop} {l : List α} :
Pairwise R l ↔ Pairwise (fun (x y : α) => x ∈ l ∧ y ∈ l ∧ R x y) l
source
theorem List.Pairwise.imp_mem {α : Type u_1} {R : α → α → Prop} {l : List α} :
Pairwise R l ↔ Pairwise (fun (x y : α) => x ∈ l → y ∈ l → R x y) l
source
theorem List.Pairwise.forall_of_forall_of_flip {α✝ : Type u_1} {l : List α✝} {R : α✝ → α✝ → Prop} (h₁ : ∀ (x : α✝), x ∈ l → R x x) (h₂ : Pairwise R l) (h₃ : Pairwise (flip R) l) ⦃x : α✝⦄ :
x ∈ l → ∀ ⦃y : α✝⦄, y ∈ l → R x y
source
theorem List.pairwise_singleton {α : Type u_1} (R : α → α → Prop) (a : α) :
Pairwise R [a]
source
theorem List.pairwise_pair {α : Type u_1} {R : α → α → Prop} {a b : α} :
Pairwise R [a, b] ↔ R a b
source
theorem List.pairwise_map {α : Type u_1} {α✝ : Type u_2} {f : α → α✝} {R : α✝ → α✝ → Prop} {l : List α} :
Pairwise R (map f l) ↔ Pairwise (fun (a b : α) => R (f a) (f b)) l
source
theorem List.Pairwise.of_map {β : Type u_1} {α : Type u_2} {R : α → α → Prop} {l : List α} {S : β → β → Prop} (f : α → β) (H : ∀ (a b : α), S (f a) (f b) → R a b) (p : Pairwise S (List.map f l)) :
Pairwise R l
source
theorem List.Pairwise.map {β : Type u_1} {α : Type u_2} {R : α → α → Prop} {l : List α} {S : β → β → Prop} (f : α → β) (H : ∀ (a b : α), R a b → S (f a) (f b)) (p : Pairwise R l) :
Pairwise S (List.map f l)
source
theorem List.pairwise_filterMap {β : Type u_1} {α : Type u_2} {R : α → α → Prop} {f : β → Option α} {l : List β} :
Pairwise R (filterMap f l) ↔ Pairwise (fun (a a' : β) => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') l
source
theorem List.Pairwise.filterMap {β : Type u_1} {α : Type u_2} {R : α → α → Prop} {S : β → β → Prop} (f : α → Option β) (H : ∀ (a a' : α), R a a' → ∀ (b : β), f a = some b → ∀ (b' : β), f a' = some b' → S b b') {l : List α} (p : Pairwise R l) :
Pairwise S (List.filterMap f l)
source
theorem List.pairwise_filter {α : Type u_1} {R : α → α → Prop} {p : α → Bool} {l : List α} :
Pairwise R (filter p l) ↔ Pairwise (fun (x y : α) => p x = true → p y = true → R x y) l
source
theorem List.Pairwise.filter {α : Type u_1} {R : α → α → Prop} {l : List α} (p : α → Bool) :
Pairwise R l → Pairwise R (List.filter p l)
source
theorem List.pairwise_append {α : Type u_1} {R : α → α → Prop} {l₁ l₂ : List α} :
Pairwise R (l₁ ++ l₂) ↔ Pairwise R l₁ ∧ Pairwise R l₂ ∧ ∀ (a : α), a ∈ l₁ → ∀ (b : α), b ∈ l₂ → R a b
source
theorem List.pairwise_append_comm {α : Type u_1} {R : α → α → Prop} (s : ∀ {x y : α}, R x y → R y x) {l₁ l₂ : List α} :
Pairwise R (l₁ ++ l₂) ↔ Pairwise R (l₂ ++ l₁)
source
theorem List.pairwise_middle {α : Type u_1} {R : α → α → Prop} (s : ∀ {x y : α}, R x y → R y x) {a : α} {l₁ l₂ : List α} :
Pairwise R (l₁ ++ a :: l₂) ↔ Pairwise R (a :: (l₁ ++ l₂))
source
theorem List.pairwise_flatten {α : Type u_1} {R : α → α → Prop} {L : List (List α)} :
Pairwise R L.flatten ↔ (∀ (l : List α), l ∈ L → Pairwise R l) ∧ Pairwise (fun (l₁ l₂ : List α) => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L
source
theorem List.pairwise_flatMap {β : Type u_1} {α : Type u_2} {R : β → β → Prop} {l : List α} {f : α → List β} :
Pairwise R (flatMap f l) ↔ (∀ (a : α), a ∈ l → Pairwise R (f a)) ∧ Pairwise (fun (a₁ a₂ : α) => ∀ (x : β), x ∈ f a₁ → ∀ (y : β), y ∈ f a₂ → R x y) l
source
theorem List.pairwise_reverse {α : Type u_1} {R : α → α → Prop} {l : List α} :
Pairwise R l.reverse ↔ Pairwise (fun (a b : α) => R b a) l
source
@[simp]
theorem List.pairwise_replicate {α : Type u_1} {R : α → α → Prop} {n : Nat} {a : α} :
Pairwise R (replicate n a) ↔ n ≤ 1 ∨ R a a
source
theorem List.Pairwise.drop {α : Type u_1} {R : α → α → Prop} {l : List α} {i : Nat} (h : Pairwise R l) :
Pairwise R (List.drop i l)
source
theorem List.Pairwise.take {α : Type u_1} {R : α → α → Prop} {l : List α} {i : Nat} (h : Pairwise R l) :
Pairwise R (List.take i l)
source
theorem List.pairwise_iff_forall_sublist {α✝ : Type u_1} {l : List α✝} {R : α✝ → α✝ → Prop} :
Pairwise R l ↔ ∀ {a b : α✝}, [a, b].Sublist l → R a b
source
theorem List.pairwise_of_forall_sublist {α✝ : Type u_1} {l : List α✝} {R : α✝ → α✝ → Prop} (g : ∀ {a b : α✝}, [a, b].Sublist l → R a b) :
Pairwise R l
source
theorem List.Pairwise.forall_sublist {α✝ : Type u_1} {l : List α✝} {R : α✝ → α✝ → Prop} (h : Pairwise R l) {a b : α✝} :
[a, b].Sublist l → R a b
source
theorem List.Pairwise.rel_of_mem_take_of_mem_drop {α : Type u_1} {R : α → α → Prop} {i : Nat} {x y : α} {l : List α} (h : Pairwise R l) (hx : x ∈ List.take i l) (hy : y ∈ List.drop i l) :
R x y
source
theorem List.Pairwise.rel_of_mem_append {α : Type u_1} {R : α → α → Prop} {x y : α} {l₁ l₂ : List α} (h : Pairwise R (l₁ ++ l₂)) (hx : x ∈ l₁) (hy : y ∈ l₂) :
R x y
source
theorem List.pairwise_of_forall_mem_list {α : Type u_1} {l : List α} {r : α → α → Prop} (h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → r a b) :
Pairwise r l
source
theorem List.pairwise_pmap {β : Type u_1} {α : Type u_2} {R : α → α → Prop} {p : β → Prop} {f : (b : β) → p b → α} {l : List β} (h : ∀ (x : β), x ∈ l → p x) :
Pairwise R (pmap f l h) ↔ Pairwise (fun (b₁ b₂ : β) => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l
source
theorem List.Pairwise.pmap {α : Type u_1} {R : α → α → Prop} {β : Type u_2} {l : List α} (hl : Pairwise R l) {p : α → Prop} {f : (a : α) → p a → β} (h : ∀ (x : α), x ∈ l → p x) {S : β → β → Prop} (hS : ∀ ⦃x : α⦄ (hx : p x) ⦃y : α⦄ (hy : p y), R x y → S (f x hx) (f y hy)) :
Pairwise S (List.pmap f l h)

### Nodup #

source
theorem List.nodup_iff_pairwise_ne {α✝ : Type u_1} {l : List α✝} :
l.Nodup ↔ Pairwise (fun (x1 x2 : α✝) => x1 ≠ x2) l
source
@[simp]
theorem List.nodup_nil {α : Type u_1} :
[].Nodup
source
@[simp]
theorem List.nodup_cons {α : Type u_1} {a : α} {l : List α} :
(a :: l).Nodup ↔ ¬a ∈ l ∧ l.Nodup
source
theorem List.nodup_append {α : Type u_1} {l₁ l₂ : List α} :
(l₁ ++ l₂).Nodup ↔ l₁.Nodup ∧ l₂.Nodup ∧ ∀ (a : α), a ∈ l₁ → ∀ (b : α), b ∈ l₂ → a ≠ b
source
theorem List.Nodup.sublist {α✝ : Type u_1} {l₁ l₂ : List α✝} :
l₁.Sublist l₂ → l₂.Nodup → l₁.Nodup
source
theorem List.Sublist.nodup {α✝ : Type u_1} {l₁ l₂ : List α✝} :
l₁.Sublist l₂ → l₂.Nodup → l₁.Nodup
source
theorem List.getElem?_inj {α : Type u_1} {i j : Nat} {xs : List α} (h₀ : i < xs.length) (h₁ : xs.Nodup) (h₂ : xs[i]? = xs[j]?) :
i = j
source
@[simp]
theorem List.nodup_replicate {α : Type u_1} {n : Nat} {a : α} :
(replicate n a).Nodup ↔ n ≤ 1
source
theorem List.Nodup.count {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : l.Nodup) :
List.count a l = if a ∈ l then 1 else 0
source
theorem List.nodup_iff_count {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} :
l.Nodup ↔ ∀ (a : α), count a l ≤ 1