# mathlib3documentation

data.list.pairwise

# Pairwise relations on a list #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides basic results about list.pairwise and list.pw_filter (definitions are in data.list.defs). pairwise r [a 0, ..., a (n - 1)] means ∀ i j, i < j → r (a i) (a j). For example, pairwise (≠) l means that all elements of l are distinct, and pairwise (<) l means that l is strictly increasing. pw_filter 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) (ᾰ : list α) :
{a : α} {l : list α}, ( (a' : α), a' l R a a') = a :: l

### Pairwise #

theorem list.rel_of_pairwise_cons {α : Type u_1} {R : α α Prop} {a : α} {l : list α} (p : (a :: l)) {a' : α} :
a' l R a a'
theorem list.pairwise.of_cons {α : Type u_1} {R : α α Prop} {a : α} {l : list α} (p : (a :: l)) :
theorem list.pairwise.tail {α : Type u_1} {R : α α Prop} {l : list α} (p : l) :
theorem list.pairwise.drop {α : Type u_1} {R : α α Prop} {l : list α} {n : } :
l)
theorem list.pairwise.imp_of_mem {α : Type u_1} {R S : α α Prop} {l : list α} (H : {a b : α}, a l b l R a b S a b) (p : l) :
theorem list.pairwise.imp {α : Type u_1} {R S : α α Prop} {l : list α} (H : (a b : α), R a b S a b) :
theorem list.pairwise_and_iff {α : Type u_1} {R S : α α Prop} {l : list α} :
list.pairwise (λ (a b : α), R a b S a b) l
theorem list.pairwise.and {α : Type u_1} {R S : α α Prop} {l : list α} (hR : l) (hS : l) :
list.pairwise (λ (a b : α), R a b S a b) 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 : l) (hS : 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)) :
theorem list.pairwise.iff {α : Type u_1} {R 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 (λ (x y : α), x l y l R x y) l
theorem list.pairwise.imp_mem {α : Type u_1} {R : α α Prop} {l : list α} :
list.pairwise (λ (x y : α), x l y l R x y) l
@[protected]
theorem list.pairwise.sublist {α : Type u_1} {R : α α Prop} {l₁ l₂ : list α} :
l₁ <+ l₂ l₂ l₁
theorem list.pairwise.forall_of_forall_of_flip {α : Type u_1} {R : α α Prop} {l : list α} (h₁ : (x : α), x l R x x) (h₂ : l) (h₃ : l) ⦃x : α⦄ :
x l ⦃y : α⦄, y l R x y
theorem list.pairwise.forall_of_forall {α : Type u_1} {R : α α Prop} {l : list α} (H : symmetric R) (H₁ : (x : α), x l R x x) (H₂ : l) ⦃x : α⦄ :
x l ⦃y : α⦄, y l R x y
theorem list.pairwise.forall {α : Type u_1} {R : α α Prop} {l : list α} (hR : symmetric R) (hl : l) ⦃a : α⦄ :
a l ⦃b : α⦄, b l a b R a b
theorem list.pairwise.set_pairwise {α : Type u_1} {R : α α Prop} {l : list α} (hl : l) (hr : symmetric R) :
{x : α | x l}.pairwise R
theorem list.pairwise_singleton {α : Type u_1} (R : α α Prop) (a : α) :
[a]
theorem list.pairwise_pair {α : Type u_1} {R : α α Prop} {a b : α} :
[a, b] R a b
theorem list.pairwise_append {α : Type u_1} {R : α α Prop} {l₁ l₂ : list α} :
(l₁ ++ l₂) l₁ l₂ (x : α), x l₁ (y : α), y l₂ R x y
theorem list.pairwise_append_comm {α : Type u_1} {R : α α Prop} (s : symmetric R) {l₁ l₂ : list α} :
(l₁ ++ l₂) (l₂ ++ l₁)
theorem list.pairwise_middle {α : Type u_1} {R : α α Prop} (s : symmetric R) {a : α} {l₁ l₂ : list α} :
(l₁ ++ a :: l₂) (a :: (l₁ ++ l₂))
theorem list.pairwise_map {α : Type u_1} {β : Type u_2} {R : α α Prop} (f : β α) {l : list β} :
(list.map f l) list.pairwise (λ (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 : (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 b S (f a) (f b)) (p : l) :
(list.map f l)
theorem list.pairwise_filter_map {α : Type u_1} {β : Type u_2} {R : α α Prop} (f : β ) {l : list β} :
l) list.pairwise (λ (a a' : β), (b : α), b f a (b' : α), b' f a' R b b') l
theorem list.pairwise.filter_map {α : Type u_1} {β : Type u_2} {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 : l) :
l)
theorem list.pairwise_filter {α : Type u_1} {R : α α Prop} (p : α Prop) {l : list α} :
l) list.pairwise (λ (x y : α), p x p y R x y) l
theorem list.pairwise.filter {α : Type u_1} {R : α α Prop} {l : list α} (p : α Prop)  :
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) :
l h) list.pairwise (λ (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 : 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)) :
l h)
theorem list.pairwise_join {α : Type u_1} {R : α α Prop} {L : list (list α)} :
( (l : list α), l L l) list.pairwise (λ (l₁ l₂ : list α), (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 β} :
(l.bind f) ( (a : α), a l (f a)) list.pairwise (λ (a₁ a₂ : α), (x : β), x f a₁ (y : β), y f a₂ R x y) l
@[simp]
theorem list.pairwise_reverse {α : Type u_1} {R : α α Prop} {l : list α} :
list.pairwise (λ (x y : α), R y x) l
theorem list.pairwise_of_reflexive_on_dupl_of_forall_ne {α : Type u_1} [decidable_eq α] {l : list α} {r : α α Prop} (hr : (a : α), 1 < l r a a) (h : (a : α), a l (b : α), b l a b r a b) :
theorem list.pairwise_of_forall_mem_list {α : Type u_1} {l : list α} {r : α α Prop} (h : (a : α), a l (b : α), b l r a b) :
theorem list.pairwise_of_reflexive_of_forall_ne {α : Type u_1} {l : list α} {r : α α Prop} (hr : reflexive r) (h : (a : α), a l (b : α), b l a b r a b) :
theorem list.pairwise_iff_nth_le {α : Type u_1} {R : α α Prop} {l : list α} :
(i j : ) (h₁ : j < l.length) (h₂ : i < j), R (l.nth_le i _) (l.nth_le j h₁)
theorem list.pairwise_replicate {α : Type u_1} {r : α α Prop} {x : α} (hx : r x x) (n : ) :
x)

### Pairwise filtering #

@[simp]
theorem list.pw_filter_nil {α : Type u_1} {R : α α Prop}  :
@[simp]
theorem list.pw_filter_cons_of_pos {α : Type u_1} {R : α α Prop} {a : α} {l : list α} (h : (b : α), b R a b) :
(a :: l) = a ::
@[simp]
theorem list.pw_filter_cons_of_neg {α : Type u_1} {R : α α Prop} {a : α} {l : list α} (h : ¬ (b : α), b R a b) :
(a :: l) =
theorem list.pw_filter_map {α : Type u_1} {β : Type u_2} {R : α α Prop} (f : β α) (l : list β) :
(list.map f l) = (list.pw_filter (λ (x y : β), R (f x) (f y)) l)
theorem list.pw_filter_sublist {α : Type u_1} {R : α α Prop} (l : list α) :
<+ l
theorem list.pw_filter_subset {α : Type u_1} {R : α α Prop} (l : list α) :
l
theorem list.pairwise_pw_filter {α : Type u_1} {R : α α Prop} (l : list α) :
l)
theorem list.pw_filter_eq_self {α : Type u_1} {R : α α Prop} {l : list α} :
= l
@[protected]
theorem list.pairwise.pw_filter {α : Type u_1} {R : α α Prop} {l : list α} :
= l

Alias of the reverse direction of list.pw_filter_eq_self.

@[simp]
theorem list.pw_filter_idempotent {α : Type u_1} {R : α α Prop} {l : list α}  :
l) =
theorem list.forall_mem_pw_filter {α : Type u_1} {R : α α Prop} (neg_trans : {x y z : α}, R x z R x y R y z) (a : α) (l : list α) :
( (b : α), b R a b) (b : α), b l R a b