Documentation

Mathlib.Data.List.Pairwise

Pairwise relations on a list #

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

theorem List.pairwise_iff {α : Type u} (R : ααProp) :
∀ (a : List α), List.Pairwise R a a = [] ∃ (a_1 : α), ∃ (l : List α), (∀ (a' : α), a' lR a_1 a') List.Pairwise R l a = a_1 :: l

Pairwise #

theorem List.Pairwise.forall_of_forall {α : Type u_1} {R : ααProp} {l : List α} (H : Symmetric R) (H₁ : ∀ (x : α), x lR x x) (H₂ : List.Pairwise R l) ⦃x : α :
x l∀ ⦃y : α⦄, y lR x y
theorem List.Pairwise.forall {α : Type u_1} {R : ααProp} {l : List α} (hR : Symmetric R) (hl : List.Pairwise R l) ⦃a : α :
a l∀ ⦃b : α⦄, b la bR a b
theorem List.Pairwise.set_pairwise {α : Type u_1} {R : ααProp} {l : List α} (hl : List.Pairwise R l) (hr : Symmetric R) :
{x : α | x l}.Pairwise R
@[deprecated]
theorem List.pairwise_map' {α : Type u_1} {β : Type u_2} {R : ααProp} (f : βα) {l : List β} :
List.Pairwise R (List.map f l) List.Pairwise (fun (a b : β) => R (f a) (f b)) l
theorem List.pairwise_pmap {α : Type u_1} {β : Type u_2} {R : ααProp} {p : βProp} {f : (b : β) → p bα} {l : List β} (h : ∀ (x : β), x lp x) :
List.Pairwise R (List.pmap f l h) List.Pairwise (fun (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 : List.Pairwise R l) {p : αProp} {f : (a : α) → p aβ} (h : ∀ (x : α), x lp x) {S : ββProp} (hS : ∀ ⦃x : α⦄ (hx : p x) ⦃y : α⦄ (hy : p y), R x yS (f x hx) (f y hy)) :
theorem List.pairwise_of_forall_mem_list {α : Type u_1} {l : List α} {r : ααProp} (h : ∀ (a : α), a l∀ (b : α), b lr 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 la br a b) :

Pairwise filtering #

theorem List.Pairwise.pwFilter {α : Type u_1} {R : ααProp} [DecidableRel R] {l : List α} :

Alias of the reverse direction of List.pwFilter_eq_self.