Documentation

Std.Data.List.Pairwise

Pairwise relations on a list #

This file provides basic results about List.Pairwise and List.pwFilter (definitions are in Std.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. 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 #

theorem List.rel_of_pairwise_cons :
∀ {α : Type u_1} {a : α} {l : List α} {R : ααProp}, List.Pairwise R (a :: l)∀ {a' : α}, a' lR a a'
theorem List.Pairwise.of_cons :
∀ {α : Type u_1} {a : α} {l : List α} {R : ααProp}, List.Pairwise R (a :: l)List.Pairwise R l
theorem List.Pairwise.tail {α : Type u_1} {R : ααProp} {l : List α} (_p : List.Pairwise R l) :
theorem List.Pairwise.drop {α : Type u_1} {R : ααProp} {l : List α} {n : Nat} :
theorem List.Pairwise.imp_of_mem {α : Type u_1} {l : List α} {R : ααProp} {S : ααProp} (H : {a b : α} → a lb lR a bS a b) (p : List.Pairwise R l) :
theorem List.Pairwise.and :
∀ {α : Type u_1} {R : ααProp} {l : List α} {S : ααProp}, List.Pairwise R lList.Pairwise S lList.Pairwise (fun a b => R a b S a b) l
theorem List.pairwise_and_iff :
∀ {α : Type u_1} {R : ααProp} {l : List α} {S : ααProp}, List.Pairwise (fun a b => R a b S a b) l List.Pairwise R l List.Pairwise S l
theorem List.Pairwise.imp₂ :
∀ {α : Type u_1} {R S T : ααProp} {l : List α}, (∀ (a b : α), R a bS a bT a b) → List.Pairwise R lList.Pairwise S lList.Pairwise T l
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 R l 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 R l List.Pairwise (fun x y => x ly lR x y) l
theorem List.Pairwise.forall_of_forall_of_flip :
∀ {α : Type u_1} {l : List α} {R : ααProp}, (∀ (x : α), x lR x x) → List.Pairwise R lList.Pairwise (flip R) l∀ ⦃x : α⦄, x l∀ ⦃y : α⦄, y lR x y
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 : {x y : α} → R x yR y x) {l₁ : List α} {l₂ : List α} :
List.Pairwise R (l₁ ++ l₂) List.Pairwise R (l₂ ++ l₁)
theorem List.pairwise_middle {α : Type u_1} {R : ααProp} (s : {x y : α} → R x yR y x) {a : α} {l₁ : List α} {l₂ : List α} :
List.Pairwise R (l₁ ++ a :: l₂) List.Pairwise R (a :: (l₁ ++ 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.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 : List.Pairwise R l) :
theorem List.pairwise_filterMap {β : Type u_1} {α : Type u_2} {R : ααProp} (f : βOption α) {l : List β} :
List.Pairwise R (List.filterMap f l) List.Pairwise (fun 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 : αOption β) (H : (a a' : α) → R a a'(b : β) → b f a(b' : β) → b' f a'S b b') {l : List α} (p : List.Pairwise R l) :
theorem List.pairwise_filter {α : Type u_1} {R : ααProp} (p : αProp) [DecidablePred p] {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) :
theorem List.pairwise_join {α : Type u_1} {R : ααProp} {L : List (List α)} :
List.Pairwise R (List.join L) (∀ (l : List α), l LList.Pairwise R 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 (List.bind l f) (∀ (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_iff_forall_sublist :
∀ {α : Type u_1} {l : List α} {R : ααProp}, List.Pairwise R l ∀ {a b : α}, List.Sublist [a, b] lR a b
@[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.map_get_sublist {α : Type u_1} {l : List α} {is : List (Fin (List.length l))} (h : List.Pairwise (fun x x_1 => x < x_1) is) :

given a list is of monotonically increasing indices into l, getting each index produces a sublist of l.

theorem List.sublist_eq_map_get :
∀ {α : Type u_1} {l' l : List α}, List.Sublist l' lis, l' = List.map (List.get l) is List.Pairwise (fun x x_1 => x < x_1) is

given a sublist l' <+ l, there exists a list of indices is such that l' = map (get l) is.

theorem List.pairwise_iff_get :
∀ {α : Type u_1} {R : ααProp} {l : List α}, List.Pairwise R l ∀ (i j : Fin (List.length l)), i < jR (List.get l i) (List.get l j)
theorem List.pairwise_replicate {α : Type u_1} {r : ααProp} {x : α} (hx : r x x) (n : Nat) :

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 α) :
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