Documentation

Batteries.Data.List.Pairwise

Pairwise relations on a list #

This file provides basic results about List.Pairwise and List.pwFilter (definitions are in Batteries.Data.List.Basic). 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. 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

Pairwise #

source
theorem List.pairwise_iff_get {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {l : List α✝} :
Pairwise R l ↔ ∀ (i j : Fin l.length), i < j → R (l.get i) (l.get j)

Pairwise filtering #

source
@[simp]
theorem List.pwFilter_nil {α✝ : Type u_1} {R : α✝ → α✝ → Prop} [DecidableRel R] :
pwFilter R [] = []
source
@[simp]
theorem List.pwFilter_cons_of_pos {α : Type u_1} {R : α → α → Prop} [DecidableRel R] {a : α} {l : List α} (h : ∀ (b : α), b ∈ pwFilter R l → R a b) :
pwFilter R (a :: l) = a :: pwFilter R l
source
@[simp]
theorem List.pwFilter_cons_of_neg {α : Type u_1} {R : α → α → Prop} [DecidableRel R] {a : α} {l : List α} (h : ¬∀ (b : α), b ∈ pwFilter R l → R a b) :
pwFilter R (a :: l) = pwFilter R l
source
theorem List.pwFilter_map {α : Type u_1} {R : α → α → Prop} {β : Type u_2} [DecidableRel R] (f : β → α) (l : List β) :
pwFilter R (map f l) = map f (pwFilter (fun (x y : β) => R (f x) (f y)) l)
source
theorem List.pwFilter_sublist {α : Type u_1} {R : α → α → Prop} [DecidableRel R] (l : List α) :
(pwFilter R l).Sublist l
source
theorem List.pwFilter_subset {α : Type u_1} {R : α → α → Prop} [DecidableRel R] (l : List α) :
pwFilter R l ⊆ l
source
theorem List.pairwise_pwFilter {α : Type u_1} {R : α → α → Prop} [DecidableRel R] (l : List α) :
Pairwise R (pwFilter R l)
source
theorem List.pwFilter_eq_self {α : Type u_1} {R : α → α → Prop} [DecidableRel R] {l : List α} :
pwFilter R l = l ↔ Pairwise R l
source
@[simp]
theorem List.pwFilter_idem {α : Type u_1} {R : α → α → Prop} {l : List α} [DecidableRel R] :
pwFilter R (pwFilter R l) = pwFilter R l
source
theorem List.forall_mem_pwFilter {α : Type u_1} {R : α → α → Prop} [DecidableRel R] (neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z) (a : α) (l : List α) :
(∀ (b : α), b ∈ pwFilter R l → R a b) ↔ ∀ (b : α), b ∈ l → R a b