Pairwise relations on a list #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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_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}
{l : list α}
(H : ∀ (a b : α), R a b → S a b) :
list.pairwise R l → list.pairwise S l
theorem
list.pairwise_and_iff
{α : 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.and
{α : Type u_1}
{R S : α → α → Prop}
{l : list α}
(hR : list.pairwise R l)
(hS : list.pairwise S l) :
list.pairwise (λ (a b : α), R a b ∧ S a b) l
theorem
list.pairwise.imp₂
{α : Type u_1}
{R S 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 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
@[protected]
theorem
list.pairwise.sublist
{α : Type u_1}
{R : α → α → Prop}
{l₁ l₂ : list α} :
l₁ <+ l₂ → list.pairwise R l₂ → list.pairwise R 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.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 : α⦄ :
theorem
list.pairwise.forall
{α : Type u_1}
{R : α → α → Prop}
{l : list α}
(hR : symmetric R)
(hl : list.pairwise R l)
⦃a : α⦄ :
theorem
list.pairwise.set_pairwise
{α : Type u_1}
{R : α → α → Prop}
{l : list α}
(hl : list.pairwise R l)
(hr : symmetric R) :
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_map
{α : Type u_1}
{β : Type u_2}
{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_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
{α : 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
{α : Type u_1}
{R : α → α → Prop}
{l : list α}
(p : α → Prop)
[decidable_pred p] :
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
theorem
list.pairwise_bind
{α : Type u_1}
{β : Type u_2}
{R : β → β → Prop}
{l : list α}
{f : α → list β} :
list.pairwise R (l.bind f) ↔ (∀ (a : α), a ∈ l → list.pairwise R (f a)) ∧ list.pairwise (λ (a₁ a₂ : α), ∀ (x : β), x ∈ f a₁ → ∀ (y : β), y ∈ f a₂ → 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_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_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
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]
@[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
@[protected]
theorem
list.pairwise.pw_filter
{α : Type u_1}
{R : α → α → Prop}
[decidable_rel R]
{l : list α} :
list.pairwise R l → list.pw_filter R l = l
Alias of the reverse direction of list.pw_filter_eq_self.
@[simp]
theorem
list.pw_filter_idempotent
{α : Type u_1}
{R : α → α → Prop}
{l : list α}
[decidable_rel R] :
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