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 : α), ∃ (l : List α), (∀ (a' : α), a' ∈ l → R a a') ∧ List.Pairwise R l ∧ a✝ = a :: l

Pairwise

theorem List.Pairwise.forall_of_forall {α : Type u_1} {R : α → α → Prop} {l : List α} (H : Symmetric R) (H₁ : ∀ (x : α), x ∈ l → R x x) (H₂ : List.Pairwise R l) ⦃x : α⦄ : x ∈ l → ∀ ⦃y : α⦄, y ∈ l → R 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 ∈ l → a ≠ b → R 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

theorem List.pairwise_of_reflexive_of_forall_ne {α : Type u_1} {l : List α} {r : α → α → Prop} (hr : Reflexive r) (h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b) : List.Pairwise r l

Pairwise filtering

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

Alias of the reverse direction of List.pwFilter_eq_self.