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 #

@[deprecated List.pairwise_iff_forall_sublist]
theorem List.pairwise_of_reflexive_on_dupl_of_forall_ne {α : Type u_1} [DecidableEq α] {l : List α} {r : ααProp} (hr : ∀ (a : α), 1 < List.count a lr a a) (h : ∀ (a : α), a l∀ (b : α), b la br a b) :
theorem List.pairwise_iff_get :
∀ {α : Type u_1} {R : ααProp} {l : List α}, List.Pairwise R l ∀ (i j : Fin l.length), i < jR (l.get i) (l.get j)

Pairwise filtering #

@[simp]
theorem List.pwFilter_nil :
∀ {α : Type u_1} {R : ααProp} [inst : DecidableRel R], List.pwFilter R [] = []
@[simp]
theorem List.pwFilter_cons_of_pos {α : Type u_1} {R : ααProp} [DecidableRel R] {a : α} {l : List α} (h : ∀ (b : α), b List.pwFilter R lR a b) :
@[simp]
theorem List.pwFilter_cons_of_neg {α : Type u_1} {R : ααProp} [DecidableRel R] {a : α} {l : List α} (h : ¬∀ (b : α), b List.pwFilter R lR a b) :
theorem List.pwFilter_map {α : Type u_1} {R : ααProp} {β : Type u_2} [DecidableRel R] (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} [DecidableRel R] (l : List α) :
(List.pwFilter R l).Sublist l
theorem List.pwFilter_subset {α : Type u_1} {R : ααProp} [DecidableRel R] (l : List α) :
theorem List.pairwise_pwFilter {α : Type u_1} {R : ααProp} [DecidableRel R] (l : List α) :
theorem List.pwFilter_eq_self {α : Type u_1} {R : ααProp} [DecidableRel R] {l : List α} :
@[simp]
theorem List.pwFilter_idem {α : Type u_1} {R : ααProp} {l : List α} [DecidableRel R] :
theorem List.forall_mem_pwFilter {α : Type u_1} {R : ααProp} [DecidableRel R] (neg_trans : ∀ {x y z : α}, R x zR x y R y z) (a : α) (l : List α) :
(∀ (b : α), b List.pwFilter R lR a b) ∀ (b : α), b lR a b