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)∀ i j, i < j → r (a i) (a j)→ r (a i) (a j). For example,
Pairwise (≠) l≠) 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}
{R : α → α → Prop}
{a : α}
{l : List α}
(p : List.Pairwise R (a :: l))
{a' : α}
:
a' ∈ l → R a a'
theorem
List.Pairwise.of_cons
{α : Type u_1}
{R : α → α → Prop}
{a : α}
{l : List α}
(p : 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)
:
List.Pairwise R (List.tail l)
theorem
List.Pairwise.drop
{α : Type u_1}
{R : α → α → Prop}
{l : List α}
{n : ℕ}
:
List.Pairwise R l → List.Pairwise R (List.drop n l)
theorem
List.Pairwise.imp_of_mem
{α : Type u_1}
{R : α → α → Prop}
{S : α → α → Prop}
{l : List α}
(H : {a b : α} → a ∈ l → b ∈ l → R a b → S a b)
(p : List.Pairwise R l)
:
List.Pairwise S l
theorem
List.pairwise_and_iff
{α : Type u_1}
{R : α → α → Prop}
{S : α → α → Prop}
{l : List α}
:
List.Pairwise (fun a b => R a b ∧ S a b) l ↔ List.Pairwise R l ∧ List.Pairwise S l
theorem
List.Pairwise.and
{α : Type u_1}
{R : α → α → Prop}
{S : α → α → Prop}
{l : List α}
(hR : List.Pairwise R l)
(hS : List.Pairwise S l)
:
List.Pairwise (fun a b => R a b ∧ S a b) l
theorem
List.Pairwise.imp₂
{α : Type u_1}
{R : α → α → Prop}
{S : α → α → Prop}
{T : α → α → Prop}
{l : List α}
(H : (a b : α) → R a b → S a b → T a b)
(hR : List.Pairwise R l)
(hS : List.Pairwise S l)
:
List.Pairwise T l
theorem
List.Pairwise.iff_of_mem
{α : Type u_1}
{R : α → α → Prop}
{S : α → α → Prop}
{l : List α}
(H : ∀ {a b : α}, a ∈ l → b ∈ l → (R a b ↔ S a b))
:
List.Pairwise R l ↔ List.Pairwise S l
theorem
List.Pairwise.iff
{α : Type u_1}
{R : α → α → Prop}
{S : α → α → Prop}
(H : ∀ (a b : α), R a b ↔ S a b)
{l : List α}
:
List.Pairwise R l ↔ List.Pairwise S l
theorem
List.pairwise_of_forall
{α : Type u_1}
{R : α → α → Prop}
{l : List α}
(H : (x y : α) → R x y)
:
List.Pairwise R l
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 ∈ l → y ∈ l → R x y) l
theorem
List.Pairwise.forall_of_forall_of_flip
{α : Type u_1}
{R : α → α → Prop}
{l : List α}
(h₁ : (x : α) → x ∈ l → R x x)
(h₂ : List.Pairwise R l)
(h₃ : List.Pairwise (flip R) l)
⦃x : α⦄
:
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
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 : Symmetric R)
{l₁ : List α}
{l₂ : List α}
:
List.Pairwise R (l₁ ++ l₂) ↔ List.Pairwise R (l₂ ++ l₁)
theorem
List.pairwise_middle
{α : Type u_1}
{R : α → α → Prop}
(s : Symmetric R)
{a : α}
{l₁ : List α}
{l₂ : List α}
:
List.Pairwise R (l₁ ++ a :: l₂) ↔ List.Pairwise R (a :: (l₁ ++ l₂))
theorem
List.pairwise_map'
{α : Type u_2}
{β : Type u_1}
{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.of_map
{α : Type u_2}
{β : Type u_1}
{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))
:
List.Pairwise R l
theorem
List.Pairwise.map
{α : Type u_1}
{β : Type u_2}
{R : α → α → Prop}
{l : List α}
{S : β → β → Prop}
(f : α → β)
(H : (a b : α) → R a b → S (f a) (f b))
(p : List.Pairwise R l)
:
List.Pairwise S (List.map f 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_2}
{β : Type u_1}
{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)
:
List.Pairwise S (List.filterMap f l)
theorem
List.pairwise_filter
{α : Type u_1}
{R : α → α → Prop}
(p : α → Prop)
[inst : DecidablePred p]
{l : List α}
:
List.Pairwise R (List.filter (fun b => decide (p b)) l) ↔ List.Pairwise (fun x y => p x → p y → R x y) l
theorem
List.Pairwise.filter
{α : Type u_1}
{R : α → α → Prop}
{l : List α}
(p : α → Bool)
:
List.Pairwise R l → List.Pairwise R (List.filter p l)
theorem
List.pairwise_pmap
{α : Type u_2}
{β : Type u_1}
{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_join
{α : Type u_1}
{R : α → α → Prop}
{L : List (List α)}
:
List.Pairwise R (List.join L) ↔ (∀ (l : List α), l ∈ L → List.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 ∈ l → List.Pairwise R (f a)) ∧ List.Pairwise (fun a₁ a₂ => (x : β) → x ∈ f a₁ → (y : β) → y ∈ f a₂ → R x y) l
theorem
List.pairwise_of_reflexive_on_dupl_of_forall_ne
{α : Type u_1}
[inst : DecidableEq α]
{l : List α}
{r : α → α → Prop}
(hr : (a : α) → 1 < List.count a l → r a a)
(h : (a : α) → a ∈ l → (b : α) → b ∈ l → a ≠ b → r a b)
:
List.Pairwise r l
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_iff_get
{α : Type u_1}
{R : α → α → Prop}
{l : List α}
:
List.Pairwise R l ↔ (i j : Fin (List.length l)) → i < j → R (List.get l i) (List.get l j)
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₁)
theorem
List.pairwise_replicate
{α : Type u_1}
{r : α → α → Prop}
{x : α}
(hx : r x x)
(n : ℕ)
:
List.Pairwise r (List.replicate n x)
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}
[inst : DecidableRel R]
{a : α}
{l : List α}
(h : (b : α) → b ∈ List.pwFilter R l → R a b)
:
List.pwFilter R (a :: l) = a :: List.pwFilter R l
@[simp]
theorem
List.pwFilter_cons_of_neg
{α : Type u_1}
{R : α → α → Prop}
[inst : DecidableRel R]
{a : α}
{l : List α}
(h : ¬((b : α) → b ∈ List.pwFilter R l → R a b))
:
List.pwFilter R (a :: l) = List.pwFilter R l
theorem
List.pwFilter_map
{α : Type u_2}
{β : Type u_1}
{R : α → α → Prop}
[inst : 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}
[inst : DecidableRel R]
(l : List α)
:
List.Sublist (List.pwFilter R l) l
theorem
List.pwFilter_subset
{α : Type u_1}
{R : α → α → Prop}
[inst : DecidableRel R]
(l : List α)
:
List.pwFilter R l ⊆ l
theorem
List.pairwise_pwFilter
{α : Type u_1}
{R : α → α → Prop}
[inst : DecidableRel R]
(l : List α)
:
List.Pairwise R (List.pwFilter R l)
theorem
List.pwFilter_eq_self
{α : Type u_1}
{R : α → α → Prop}
[inst : DecidableRel R]
{l : List α}
:
List.pwFilter R l = l ↔ List.Pairwise R l
theorem
List.Pairwise.pwFilter
{α : Type u_1}
{R : α → α → Prop}
[inst : DecidableRel R]
{l : List α}
:
List.Pairwise R l → List.pwFilter R l = l
Alias of the reverse direction of List.pwFilter_eq_self.
@[simp]
theorem
List.pwFilter_idempotent
{α : Type u_1}
{R : α → α → Prop}
{l : List α}
[inst : DecidableRel R]
:
List.pwFilter R (List.pwFilter R l) = List.pwFilter R l
theorem
List.forall_mem_pwFilter
{α : Type u_1}
{R : α → α → Prop}
[inst : DecidableRel R]
(neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z)
(a : α)
(l : List α)
:
((b : α) → b ∈ List.pwFilter R l → R a b) ↔ (b : α) → b ∈ l → R a b