# Documentation

Mathlib.Data.List.Pairwise

# Pairwise relations on a list #

This file provides basic results about List.Pairwise and List.pwFilter (definitions are in Data.List.Defs). Pairwise r [a 0, ..., a (n - 1)] means ∀ i j, i < j → r (a i) (a j)∀ i j, i < j → r (a i) (a j)→ r (a i) (a j). For example, Pairwise (≠) l≠) l means that all elements of l are distinct, and Pairwise (<) l means that l is strictly increasing. pwFilter r l is the list obtained by iteratively adding each element of l that doesn't break the pairwiseness of the list we have so far. It thus yields l' a maximal sublist of l such that Pairwise r l'.

## Tags #

sorted, nodup

theorem List.pairwise_iff {α : Type u_1} (R : ααProp) :
∀ (a : List α), a = [] Exists fun {a_1} => Exists fun {l} => ((a' : α) → a' lR a_1 a') a = a_1 :: l

### Pairwise #

theorem List.rel_of_pairwise_cons {α : Type u_1} {R : ααProp} {a : α} {l : List α} (p : List.Pairwise R (a :: l)) {a' : α} :
a' lR a a'
theorem List.Pairwise.of_cons {α : Type u_1} {R : ααProp} {a : α} {l : List α} (p : List.Pairwise R (a :: l)) :
theorem List.Pairwise.tail {α : Type u_1} {R : ααProp} {l : List α} (_p : ) :
theorem List.Pairwise.drop {α : Type u_1} {R : ααProp} {l : List α} {n : } :
List.Pairwise R ()
theorem List.Pairwise.imp_of_mem {α : Type u_1} {R : ααProp} {S : ααProp} {l : List α} (H : {a b : α} → a lb lR a bS a b) (p : ) :
theorem List.pairwise_and_iff {α : Type u_1} {R : ααProp} {S : ααProp} {l : List α} :
List.Pairwise (fun a b => R a b S a b) l
theorem List.Pairwise.and {α : Type u_1} {R : ααProp} {S : ααProp} {l : List α} (hR : ) (hS : ) :
List.Pairwise (fun a b => R a b S a b) l
theorem List.Pairwise.imp₂ {α : Type u_1} {R : ααProp} {S : ααProp} {T : ααProp} {l : List α} (H : (a b : α) → R a bS a bT a b) (hR : ) (hS : ) :
theorem List.Pairwise.iff_of_mem {α : Type u_1} {R : ααProp} {S : ααProp} {l : List α} (H : ∀ {a b : α}, a lb l → (R a b S a b)) :
theorem List.Pairwise.iff {α : Type u_1} {R : ααProp} {S : ααProp} (H : ∀ (a b : α), R a b S a b) {l : List α} :
theorem List.pairwise_of_forall {α : Type u_1} {R : ααProp} {l : List α} (H : (x y : α) → R x y) :
theorem List.Pairwise.and_mem {α : Type u_1} {R : ααProp} {l : List α} :
List.Pairwise (fun x y => x l y l R x y) l
theorem List.Pairwise.imp_mem {α : Type u_1} {R : ααProp} {l : List α} :
List.Pairwise (fun x y => x ly lR x y) l
theorem List.Pairwise.forall_of_forall_of_flip {α : Type u_1} {R : ααProp} {l : List α} (h₁ : (x : α) → x lR x x) (h₂ : ) (h₃ : List.Pairwise (flip R) l) ⦃x : α :
x ly : α⦄ → y lR x y
theorem List.Pairwise.forall_of_forall {α : Type u_1} {R : ααProp} {l : List α} (H : ) (H₁ : (x : α) → x lR x x) (H₂ : ) ⦃x : α :
x ly : α⦄ → y lR x y
theorem List.Pairwise.forall {α : Type u_1} {R : ααProp} {l : List α} (hR : ) (hl : ) ⦃a : α :
a lb : α⦄ → b la bR a b
theorem List.Pairwise.set_pairwise {α : Type u_1} {R : ααProp} {l : List α} (hl : ) (hr : ) :
Set.Pairwise { x | x l } R
theorem List.pairwise_singleton {α : Type u_1} (R : ααProp) (a : α) :
theorem List.pairwise_pair {α : Type u_1} {R : ααProp} {a : α} {b : α} :
List.Pairwise R [a, b] R a b
theorem List.pairwise_append_comm {α : Type u_1} {R : ααProp} (s : ) {l₁ : List α} {l₂ : List α} :
List.Pairwise R (l₁ ++ l₂) List.Pairwise R (l₂ ++ l₁)
theorem List.pairwise_middle {α : Type u_1} {R : ααProp} (s : ) {a : α} {l₁ : List α} {l₂ : List α} :
List.Pairwise R (l₁ ++ a :: l₂) List.Pairwise R (a :: (l₁ ++ l₂))
theorem List.pairwise_map' {α : Type u_2} {β : Type u_1} {R : ααProp} (f : βα) {l : List β} :
List.Pairwise R (List.map f l) List.Pairwise (fun a b => R (f a) (f b)) l
theorem List.Pairwise.of_map {α : Type u_2} {β : Type u_1} {R : ααProp} {l : List α} {S : ββProp} (f : αβ) (H : (a b : α) → S (f a) (f b)R a b) (p : List.Pairwise S (List.map f l)) :
theorem List.Pairwise.map {α : Type u_1} {β : Type u_2} {R : ααProp} {l : List α} {S : ββProp} (f : αβ) (H : (a b : α) → R a bS (f a) (f b)) (p : ) :
theorem List.pairwise_filterMap {α : Type u_1} {β : Type u_2} {R : ααProp} (f : β) {l : List β} :
List.Pairwise R () List.Pairwise (fun a a' => (b : α) → b f a(b' : α) → b' f a'R b b') l
theorem List.Pairwise.filter_map {α : Type u_2} {β : Type u_1} {R : ααProp} {S : ββProp} (f : α) (H : (a a' : α) → R a a'(b : β) → b f a(b' : β) → b' f a'S b b') {l : List α} (p : ) :
theorem List.pairwise_filter {α : Type u_1} {R : ααProp} (p : αProp) [inst : ] {l : List α} :
List.Pairwise R (List.filter (fun b => decide (p b)) l) List.Pairwise (fun x y => p xp yR x y) l
theorem List.Pairwise.filter {α : Type u_1} {R : ααProp} {l : List α} (p : αBool) :
List.Pairwise R ()
theorem List.pairwise_pmap {α : Type u_2} {β : Type u_1} {R : ααProp} {p : βProp} {f : (b : β) → p bα} {l : List β} (h : (x : β) → x lp x) :
List.Pairwise R (List.pmap f l h) List.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} {β : Type u_2} {R : ααProp} {l : List α} (hl : ) {p : αProp} {f : (a : α) → p aβ} (h : (x : α) → x lp x) {S : ββProp} (hS : x : α⦄ → (hx : p x) → y : α⦄ → (hy : p y) → R x yS (f x hx) (f y hy)) :
theorem List.pairwise_join {α : Type u_1} {R : ααProp} {L : List (List α)} :
(∀ (l : List α), l L) List.Pairwise (fun l₁ l₂ => (x : α) → x l₁(y : α) → y l₂R x y) L
theorem List.pairwise_bind {α : Type u_1} {β : Type u_2} {R : ββProp} {l : List α} {f : αList β} :
List.Pairwise R () (∀ (a : α), a lList.Pairwise R (f a)) List.Pairwise (fun a₁ a₂ => (x : β) → x f a₁(y : β) → y f a₂R x y) l
theorem List.pairwise_of_reflexive_on_dupl_of_forall_ne {α : Type u_1} [inst : ] {l : List α} {r : ααProp} (hr : (a : α) → 1 < r a a) (h : (a : α) → a l(b : α) → b la br a b) :
theorem List.pairwise_of_forall_mem_list {α : Type u_1} {l : List α} {r : ααProp} (h : (a : α) → a l(b : α) → b lr a b) :
theorem List.pairwise_of_reflexive_of_forall_ne {α : Type u_1} {l : List α} {r : ααProp} (hr : ) (h : (a : α) → a l(b : α) → b la br a b) :
theorem List.pairwise_iff_get {α : Type u_1} {R : ααProp} {l : List α} :
(i j : Fin ()) → i < jR (List.get l i) (List.get l j)
theorem List.pairwise_iff_nthLe {α : Type u_1} {R : ααProp} {l : List α} :
(i j : ) → (h₁ : j < ) → (h₂ : i < j) → R (List.nthLe l i (_ : i < )) (List.nthLe l j h₁)
theorem List.pairwise_replicate {α : Type u_1} {r : ααProp} {x : α} (hx : r x x) (n : ) :

### Pairwise filtering #

@[simp]
theorem List.pwFilter_nil {α : Type u_1} {R : ααProp} [inst : ] :
= []
@[simp]
theorem List.pwFilter_cons_of_pos {α : Type u_1} {R : ααProp} [inst : ] {a : α} {l : List α} (h : (b : α) → b R a b) :
List.pwFilter R (a :: l) = a ::
@[simp]
theorem List.pwFilter_cons_of_neg {α : Type u_1} {R : ααProp} [inst : ] {a : α} {l : List α} (h : ¬((b : α) → b R a b)) :
List.pwFilter R (a :: l) =
theorem List.pwFilter_map {α : Type u_2} {β : Type u_1} {R : ααProp} [inst : ] (f : βα) (l : List β) :
List.pwFilter R (List.map f l) = List.map f (List.pwFilter (fun x y => R (f x) (f y)) l)
theorem List.pwFilter_sublist {α : Type u_1} {R : ααProp} [inst : ] (l : List α) :
theorem List.pwFilter_subset {α : Type u_1} {R : ααProp} [inst : ] (l : List α) :
l
theorem List.pairwise_pwFilter {α : Type u_1} {R : ααProp} [inst : ] (l : List α) :
theorem List.pwFilter_eq_self {α : Type u_1} {R : ααProp} [inst : ] {l : List α} :
= l
theorem List.Pairwise.pwFilter {α : Type u_1} {R : ααProp} [inst : ] {l : List α} :
= l

Alias of the reverse direction of List.pwFilter_eq_self.

@[simp]
theorem List.pwFilter_idempotent {α : Type u_1} {R : ααProp} {l : List α} [inst : ] :
theorem List.forall_mem_pwFilter {α : Type u_1} {R : ααProp} [inst : ] (neg_trans : ∀ {x y z : α}, R x zR x y R y z) (a : α) (l : List α) :
((b : α) → b R a b) (b : α) → b lR a b