Pairwise relations on a list #
This file provides basic results about list.pairwise and list.pw_filter (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.
pw_filter 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_pairwise_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 l.tail
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 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.imp
{α : Type u_1}
{R S : α → α → Prop}
(H : ∀ (a b : α), R a b → S a b)
{l : list α} :
list.pairwise R l → list.pairwise S l
theorem
list.pairwise.and
{α : Type u_1}
{R S : α → α → Prop}
{l : list α} :
list.pairwise (λ (a b : α), R a b ∧ S a b) l ↔ list.pairwise R l ∧ list.pairwise S l
theorem
list.pairwise.imp₂
{α : Type u_1}
{R S T : α → α → Prop}
(H : ∀ (a b : α), R a b → S a b → T a b)
{l : list α}
(hR : list.pairwise R l)
(hS : list.pairwise S l) :
list.pairwise T l
theorem
list.pairwise.iff_of_mem
{α : Type u_1}
{R 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 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 (λ (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 (λ (x y : α), x ∈ l → y ∈ l → R x y) l
theorem
list.pairwise_of_sublist
{α : Type u_1}
{R : α → α → Prop}
{l₁ l₂ : list α} :
l₁ <+ l₂ → list.pairwise R l₂ → list.pairwise R l₁
theorem
list.forall_of_forall_of_pairwise
{α : Type u_1}
{R : α → α → Prop}
(H : symmetric R)
{l : list α}
(H₁ : ∀ (x : α), x ∈ l → R x x)
(H₂ : list.pairwise R l)
(x : α)
(H_1 : x ∈ l)
(y : α)
(H_2 : y ∈ l) :
R x y
theorem
list.forall_of_pairwise
{α : Type u_1}
{R : α → α → Prop}
(H : symmetric R)
{l : list α}
(hl : list.pairwise R l)
(a : α)
(H_1 : a ∈ l)
(b : α)
(H_2 : b ∈ l) :
a ≠ b → R a b
theorem
list.pairwise_pair
{α : Type u_1}
{R : α → α → Prop}
{a b : α} :
list.pairwise R [a, b] ↔ R a b
theorem
list.pairwise_append
{α : Type u_1}
{R : α → α → Prop}
{l₁ l₂ : list α} :
list.pairwise R (l₁ ++ l₂) ↔ list.pairwise R l₁ ∧ list.pairwise R l₂ ∧ ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y
theorem
list.pairwise_append_comm
{α : Type u_1}
{R : α → α → Prop}
(s : symmetric R)
{l₁ 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₁ l₂ : list α} :
list.pairwise R (l₁ ++ a :: l₂) ↔ list.pairwise R (a :: (l₁ ++ l₂))
theorem
list.pairwise_map
{α : Type u_1}
{β : Type u_2}
{R : α → α → Prop}
(f : β → α)
{l : list β} :
list.pairwise R (list.map f l) ↔ list.pairwise (λ (a b : β), R (f a) (f b)) l
theorem
list.pairwise_of_pairwise_map
{α : Type u_1}
{β : Type u_2}
{R : α → α → Prop}
{S : β → β → Prop}
(f : α → β)
(H : ∀ (a b : α), S (f a) (f b) → R a b)
{l : list α}
(p : list.pairwise S (list.map f l)) :
list.pairwise R l
theorem
list.pairwise_map_of_pairwise
{α : Type u_1}
{β : Type u_2}
{R : α → α → Prop}
{S : β → β → Prop}
(f : α → β)
(H : ∀ (a b : α), R a b → S (f a) (f b))
{l : list α}
(p : list.pairwise R l) :
list.pairwise S (list.map f l)
theorem
list.pairwise_filter_map
{α : Type u_1}
{β : Type u_2}
{R : α → α → Prop}
(f : β → option α)
{l : list β} :
list.pairwise R (list.filter_map f l) ↔ list.pairwise (λ (a a' : β), ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b') l
theorem
list.pairwise_filter_map_of_pairwise
{α : Type u_1}
{β : Type u_2}
{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.filter_map f l)
theorem
list.pairwise_filter
{α : Type u_1}
{R : α → α → Prop}
(p : α → Prop)
[decidable_pred p]
{l : list α} :
list.pairwise R (list.filter p l) ↔ list.pairwise (λ (x y : α), p x → p y → R x y) l
theorem
list.pairwise_filter_of_pairwise
{α : Type u_1}
{R : α → α → Prop}
(p : α → Prop)
[decidable_pred p]
{l : list α} :
list.pairwise R l → list.pairwise R (list.filter p 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 (λ (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 L.join ↔ (∀ (l : list α), l ∈ L → list.pairwise R l) ∧ list.pairwise (λ (l₁ l₂ : list α), ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L
@[simp]
theorem
list.pairwise_reverse
{α : Type u_1}
{R : α → α → Prop}
{l : list α} :
list.pairwise R l.reverse ↔ list.pairwise (λ (x y : α), R y x) l
theorem
list.pairwise.set_pairwise
{α : Type u_1}
{R : α → α → Prop}
{l : list α}
(h : list.pairwise R l)
(hr : symmetric R) :
theorem
list.pairwise_of_reflexive_on_dupl_of_forall_ne
{α : Type u_1}
[decidable_eq α]
{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_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
theorem
list.pairwise_sublists'
{α : Type u_1}
{R : α → α → Prop}
{l : list α} :
list.pairwise R l → list.pairwise (list.lex (function.swap R)) l.sublists'
theorem
list.pairwise_sublists
{α : Type u_1}
{R : α → α → Prop}
{l : list α}
(H : list.pairwise R l) :
Pairwise filtering #
@[simp]
@[simp]
theorem
list.pw_filter_cons_of_pos
{α : Type u_1}
{R : α → α → Prop}
[decidable_rel R]
{a : α}
{l : list α}
(h : ∀ (b : α), b ∈ list.pw_filter R l → R a b) :
list.pw_filter R (a :: l) = a :: list.pw_filter R l
@[simp]
theorem
list.pw_filter_cons_of_neg
{α : Type u_1}
{R : α → α → Prop}
[decidable_rel R]
{a : α}
{l : list α}
(h : ¬∀ (b : α), b ∈ list.pw_filter R l → R a b) :
list.pw_filter R (a :: l) = list.pw_filter R l
theorem
list.pw_filter_map
{α : Type u_1}
{β : Type u_2}
{R : α → α → Prop}
[decidable_rel R]
(f : β → α)
(l : list β) :
list.pw_filter R (list.map f l) = list.map f (list.pw_filter (λ (x y : β), R (f x) (f y)) l)
theorem
list.pw_filter_sublist
{α : Type u_1}
{R : α → α → Prop}
[decidable_rel R]
(l : list α) :
list.pw_filter R l <+ l
theorem
list.pw_filter_subset
{α : Type u_1}
{R : α → α → Prop}
[decidable_rel R]
(l : list α) :
list.pw_filter R l ⊆ l
theorem
list.pairwise_pw_filter
{α : Type u_1}
{R : α → α → Prop}
[decidable_rel R]
(l : list α) :
list.pairwise R (list.pw_filter R l)
theorem
list.pw_filter_eq_self
{α : Type u_1}
{R : α → α → Prop}
[decidable_rel R]
{l : list α} :
list.pw_filter R l = l ↔ list.pairwise R l
@[simp]
theorem
list.pw_filter_idempotent
{α : Type u_1}
{R : α → α → Prop}
[decidable_rel R]
{l : list α} :
list.pw_filter R (list.pw_filter R l) = list.pw_filter R l
theorem
list.forall_mem_pw_filter
{α : Type u_1}
{R : α → α → Prop}
[decidable_rel R]
(neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z)
(a : α)
(l : list α) :
(∀ (b : α), b ∈ list.pw_filter R l → R a b) ↔ ∀ (b : α), b ∈ l → R a b