Lemmas about List.Pairwise and List.Nodup.

Pairwise and Nodup

Pairwise

theorem List.Pairwise.sublist {α✝ : Type u_1} {l₁ l₂ : List α✝} {R : α✝ → α✝ → Prop} : l₁.Sublist l₂ → Pairwise R l₂ → Pairwise R l₁

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

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'

theorem List.Pairwise.of_cons {α✝ : Type u_1} {a : α✝} {l : List α✝} {R : α✝ → α✝ → Prop} (p : Pairwise R (a :: l)) : Pairwise R l

theorem List.Pairwise.tail {α : Type u_1} {R : α → α → Prop} {l : List α} (h : Pairwise R l) : Pairwise R l.tail

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

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

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

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

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

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

theorem List.pairwise_of_forall {α : Type u_1} {R : α → α → Prop} {l : List α} (H : ∀ (x y : α), R x y) : Pairwise R l

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

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

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

theorem List.pairwise_singleton {α : Type u_1} (R : α → α → Prop) (a : α) : Pairwise R [a]

theorem List.pairwise_pair {α : Type u_1} {R : α → α → Prop} {a b : α} : Pairwise R [a, b] ↔ R a b

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

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

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)

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 : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b') l

theorem List.Pairwise.filterMap {β : Type u_1} {α : Type u_2} {R : α → α → Prop} {S : β → β → Prop} (f : α → Option β) (H : ∀ (a a' : α), R a a' → ∀ (b : β), b ∈ f a → ∀ (b' : β), b' ∈ f a' → S b b') {l : List α} (p : Pairwise R l) : Pairwise S (List.filterMap f l)

theorem List.pairwise_filter {α : Type u_1} {R : α → α → Prop} {p : α → Prop} [DecidablePred p] {l : List α} : Pairwise R (filter (fun (b : α) => decide (p b)) l) ↔ Pairwise (fun (x y : α) => p x → p y → R x y) l

theorem List.Pairwise.filter {α : Type u_1} {R : α → α → Prop} {l : List α} (p : α → Bool) : Pairwise R l → Pairwise R (List.filter p l)

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

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₁)

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₂))

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

@[reducible, inline, deprecated List.pairwise_flatten (since := "2024-10-14")]

abbrev List.pairwise_join {α : 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

Equations

• @List.pairwise_join = @List.pairwise_flatten

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

@[reducible, inline, deprecated List.pairwise_flatMap (since := "2024-10-14")]

abbrev List.pairwise_bind {β : 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

Equations

• @List.pairwise_bind = @List.pairwise_flatMap

theorem List.pairwise_reverse {α : Type u_1} {R : α → α → Prop} {l : List α} : Pairwise R l.reverse ↔ Pairwise (fun (a b : α) => R b a) l

@[simp]

theorem List.pairwise_replicate {α : Type u_1} {R : α → α → Prop} {n : Nat} {a : α} : Pairwise R (replicate n a) ↔ n ≤ 1 ∨ R a a

theorem List.Pairwise.drop {α : Type u_1} {R : α → α → Prop} {l : List α} {i : Nat} (h : Pairwise R l) : Pairwise R (List.drop i l)

theorem List.Pairwise.take {α : Type u_1} {R : α → α → Prop} {l : List α} {i : Nat} (h : Pairwise R l) : Pairwise R (List.take i l)

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

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

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

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

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

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

@[simp]

theorem List.nodup_nil {α : Type u_1} : [].Nodup

@[simp]

theorem List.nodup_cons {α : Type u_1} {a : α} {l : List α} : (a :: l).Nodup ↔ ¬a ∈ l ∧ l.Nodup

theorem List.Nodup.sublist {α✝ : Type u_1} {l₁ l₂ : List α✝} : l₁.Sublist l₂ → l₂.Nodup → l₁.Nodup

theorem List.Sublist.nodup {α✝ : Type u_1} {l₁ l₂ : List α✝} : l₁.Sublist l₂ → l₂.Nodup → l₁.Nodup

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

@[simp]

theorem List.nodup_replicate {α : Type u_1} {n : Nat} {a : α} : (replicate n a).Nodup ↔ n ≤ 1