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 #
theorem
List.pairwise_iff_get
{α✝ : Type u_1}
{R : α✝ → α✝ → Prop}
{l : List α✝}
:
Pairwise R l ↔ ∀ (i j : Fin l.length), i < j → R (l.get i) (l.get j)
Pairwise filtering #
@[simp]
@[simp]
@[simp]
theorem
List.pwFilter_sublist
{α : Type u_1}
{R : α → α → Prop}
[DecidableRel R]
(l : List α)
:
(pwFilter R l).Sublist l
theorem
List.pwFilter_subset
{α : Type u_1}
{R : α → α → Prop}
[DecidableRel R]
(l : List α)
:
pwFilter R l ⊆ l
theorem
List.pairwise_pwFilter
{α : Type u_1}
{R : α → α → Prop}
[DecidableRel R]
(l : List α)
:
Pairwise R (pwFilter R l)
theorem
List.pwFilter_eq_self
{α : Type u_1}
{R : α → α → Prop}
[DecidableRel R]
{l : List α}
:
pwFilter R l = l ↔ Pairwise R l
@[simp]
theorem
List.forall_mem_pwFilter
{α : Type u_1}
{R : α → α → Prop}
[DecidableRel R]
(neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z)
(a : α)
(l : List α)
:
(∀ (b : α), b ∈ pwFilter R l → R a b) ↔ ∀ (b : α), b ∈ l → R a b