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_1} (R : α → α → Prop) : ∀ (a : List α), List.Pairwise R a ↔ a = [] ∨ ∃ a_1 l, ((a' : α) → a' ∈ l → R 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 ∈ 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) : Set.Pairwise {x | x ∈ l} 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 ∈ l → p 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 ∈ l → p x) {S : β → β → Prop} (hS : ⦃x : α⦄ → (hx : p x) → ⦃y : α⦄ → (hy : p y) → R x y → S (f x hx) (f y hy)) : List.Pairwise S (List.pmap f l h)

theorem List.pairwise_of_forall_mem_list {α : Type u_1} {l : List α} {r : α → α → Prop} (h : (a : α) → a ∈ l → (b : α) → b ∈ l → r a b) : List.Pairwise r l

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

@[deprecated List.pairwise_iff_get]

theorem List.pairwise_iff_nthLe {α : Type u_1} {R : α → α → Prop} {l : List α} : List.Pairwise R l ↔ (i j : ℕ) → (h₁ : j < List.length l) → (h₂ : i < j) → R (List.nthLe l i (_ : i < List.length l)) (List.nthLe l j h₁)

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.