mathlib documentation

data.list.pairwise

theorem list.rel_of_pairwise_cons {α : Type u} {R : α → α → Prop} {a : α} {l : list α} (p : list.pairwise R (a :: l)) {a' : α} :
a' lR a a'

theorem list.pairwise_of_pairwise_cons {α : Type u} {R : α → α → Prop} {a : α} {l : list α} :

theorem list.pairwise.imp_of_mem {α : Type u} {R S : α → α → Prop} {l : list α} :
(∀ {a b : α}, a lb lR a bS a b)list.pairwise R llist.pairwise S l

theorem list.pairwise.imp {α : Type u} {R S : α → α → Prop} (H : ∀ (a b : α), R a bS a b) {l : list α} :

theorem list.pairwise.and {α : Type u} {R S : α → α → Prop} {l : list α} :
list.pairwise (λ (a b : α), R a b S a b) l list.pairwise R l list.pairwise S l

theorem list.pairwise.imp₂ {α : Type u} {R S T : α → α → Prop} (H : ∀ (a b : α), R a bS a bT a b) {l : list α} :

theorem list.pairwise.iff_of_mem {α : Type u} {R S : α → α → Prop} {l : list α} :
(∀ {a b : α}, a lb l(R a b S a b))(list.pairwise R l list.pairwise S l)

theorem list.pairwise.iff {α : Type u} {R S : α → α → Prop} (H : ∀ (a b : α), R a b S a b) {l : list α} :

theorem list.pairwise_of_forall {α : Type u} {R : α → α → Prop} {l : list α} :
(∀ (x y : α), R x y)list.pairwise R l

theorem list.pairwise.and_mem {α : Type u} {R : α → α → Prop} {l : list α} :
list.pairwise R l list.pairwise (λ (x y : α), x l y l R x y) l

theorem list.pairwise.imp_mem {α : Type u} {R : α → α → Prop} {l : list α} :
list.pairwise R l list.pairwise (λ (x y : α), x ly lR x y) l

theorem list.pairwise_of_sublist {α : Type u} {R : α → α → Prop} {l₁ l₂ : list α} :
l₁ <+ l₂list.pairwise R l₂list.pairwise R l₁

theorem list.forall_of_forall_of_pairwise {α : Type u} {R : α → α → Prop} (H : symmetric R) {l : list α} (H₁ : ∀ (x : α), x lR x x) (H₂ : list.pairwise R l) (x : α) (H_1 : x l) (y : α) :
y lR x y

theorem list.forall_of_pairwise {α : Type u} {R : α → α → Prop} (H : symmetric R) {l : list α} (hl : list.pairwise R l) (a : α) (H_1 : a l) (b : α) :
b la bR a b

theorem list.pairwise_singleton {α : Type u} (R : α → α → Prop) (a : α) :

theorem list.pairwise_pair {α : Type u} {R : α → α → Prop} {a b : α} :
list.pairwise R [a, b] R a b

theorem list.pairwise_append {α : Type u} {R : α → α → Prop} {l₁ l₂ : list α} :
list.pairwise R (l₁ ++ l₂) list.pairwise R l₁ list.pairwise R l₂ ∀ (x : α), x l₁∀ (y : α), y l₂R x y

theorem list.pairwise_append_comm {α : Type u} {R : α → α → Prop} (s : symmetric R) {l₁ l₂ : list α} :
list.pairwise R (l₁ ++ l₂) list.pairwise R (l₂ ++ l₁)

theorem list.pairwise_middle {α : Type u} {R : α → α → Prop} (s : symmetric R) {a : α} {l₁ l₂ : list α} :
list.pairwise R (l₁ ++ a :: l₂) list.pairwise R (a :: (l₁ ++ l₂))

theorem list.pairwise_map {α : Type u} {β : Type v} {R : α → α → Prop} (f : β → α) {l : list β} :
list.pairwise R (list.map f l) list.pairwise (λ (a b : β), R (f a) (f b)) l

theorem list.pairwise_of_pairwise_map {α : Type u} {β : Type v} {R : α → α → Prop} {S : β → β → Prop} (f : α → β) (H : ∀ (a b : α), S (f a) (f b)R a b) {l : list α} :

theorem list.pairwise_map_of_pairwise {α : Type u} {β : Type v} {R : α → α → Prop} {S : β → β → Prop} (f : α → β) (H : ∀ (a b : α), R a bS (f a) (f b)) {l : list α} :

theorem list.pairwise_filter_map {α : Type u} {β : Type v} {R : α → α → Prop} (f : β → option α) {l : list β} :
list.pairwise R (list.filter_map f l) list.pairwise (λ (a a' : β), ∀ (b : α), b f a∀ (b' : α), b' f a'R b b') l

theorem list.pairwise_filter_map_of_pairwise {α : Type u} {β : Type v} {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 α} :

theorem list.pairwise_filter {α : Type u} {R : α → α → Prop} (p : α → Prop) [decidable_pred p] {l : list α} :
list.pairwise R (list.filter p l) list.pairwise (λ (x y : α), p xp yR x y) l

theorem list.pairwise_filter_of_pairwise {α : Type u} {R : α → α → Prop} (p : α → Prop) [decidable_pred p] {l : list α} :

theorem list.pairwise_join {α : Type u} {R : α → α → Prop} {L : list (list α)} :
list.pairwise R L.join (∀ (l : list α), l Llist.pairwise R l) list.pairwise (λ (l₁ l₂ : list α), ∀ (x : α), x l₁∀ (y : α), y l₂R x y) L

@[simp]
theorem list.pairwise_reverse {α : Type u} {R : α → α → Prop} {l : list α} :
list.pairwise R l.reverse list.pairwise (λ (x y : α), R y x) l

theorem list.pairwise_iff_nth_le {α : Type u} {R : α → α → Prop} {l : list α} :
list.pairwise R l ∀ (i j : ) (h₁ : j < l.length) (h₂ : i < j), R (l.nth_le i _) (l.nth_le j h₁)

theorem list.pairwise_sublists' {α : Type u} {R : α → α → Prop} {l : list α} :

theorem list.pairwise_sublists {α : Type u} {R : α → α → Prop} {l : list α} :
list.pairwise R llist.pairwise (λ (l₁ l₂ : list α), list.lex R l₁.reverse l₂.reverse) l.sublists

@[simp]
theorem list.pw_filter_nil {α : Type u} {R : α → α → Prop} [decidable_rel R] :

@[simp]
theorem list.pw_filter_cons_of_pos {α : Type u} {R : α → α → Prop} [decidable_rel R] {a : α} {l : list α} :
(∀ (b : α), b list.pw_filter R lR a b)list.pw_filter R (a :: l) = a :: list.pw_filter R l

@[simp]
theorem list.pw_filter_cons_of_neg {α : Type u} {R : α → α → Prop} [decidable_rel R] {a : α} {l : list α} :
(¬∀ (b : α), b list.pw_filter R lR a b)list.pw_filter R (a :: l) = list.pw_filter R l

theorem list.pw_filter_map {α : Type u} {β : Type v} {R : α → α → Prop} [decidable_rel R] (f : β → α) (l : list β) :
list.pw_filter R (list.map f l) = list.map f (list.pw_filter (λ (x y : β), R (f x) (f y)) l)

theorem list.pw_filter_sublist {α : Type u} {R : α → α → Prop} [decidable_rel R] (l : list α) :

theorem list.pw_filter_subset {α : Type u} {R : α → α → Prop} [decidable_rel R] (l : list α) :

theorem list.pairwise_pw_filter {α : Type u} {R : α → α → Prop} [decidable_rel R] (l : list α) :

theorem list.pw_filter_eq_self {α : Type u} {R : α → α → Prop} [decidable_rel R] {l : list α} :

@[simp]
theorem list.pw_filter_idempotent {α : Type u} {R : α → α → Prop} [decidable_rel R] {l : list α} :

theorem list.forall_mem_pw_filter {α : Type u} {R : α → α → Prop} [decidable_rel R] (neg_trans : ∀ {x y z : α}, R x zR x y R y z) (a : α) (l : list α) :
(∀ (b : α), b list.pw_filter R lR a b) ∀ (b : α), b lR a b