Pairwise relations on a list #
This file provides basic results about List.Pairwise and List.pwFilter (definitions are in
Std.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.of_cons :
∀ {α : Type u_1} {a : α} {l : List α} {R : α → α → Prop}, 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 : Nat}
:
List.Pairwise R l → List.Pairwise R (List.drop n l)
theorem
List.Pairwise.imp_of_mem
{α : Type u_1}
{l : List α}
{R : α → α → Prop}
{S : α → α → Prop}
(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 :
∀ {α : Type u_1} {R : α → α → Prop} {l : List α} {S : α → α → Prop},
List.Pairwise R l → List.Pairwise S l → List.Pairwise (fun (a b : α) => R a b ∧ S a b) l
theorem
List.pairwise_and_iff :
∀ {α : Type u_1} {R : α → α → Prop} {l : List α} {S : α → α → Prop},
List.Pairwise (fun (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} {l : List α},
(∀ (a b : α), R a b → S a b → T a b) → List.Pairwise R l → 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} {l : List α} {R : α → α → Prop},
(∀ (x : α), x ∈ l → R x x) →
List.Pairwise R l → List.Pairwise (flip R) l → ∀ ⦃x : α⦄, x ∈ l → ∀ ⦃y : α⦄, y ∈ l → R x y
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 : ∀ {x y : α}, R x y → R y x)
{l₁ : List α}
{l₂ : List α}
:
List.Pairwise R (l₁ ++ l₂) ↔ List.Pairwise R (l₂ ++ l₁)
theorem
List.pairwise_middle
{α : Type u_1}
{R : α → α → Prop}
(s : ∀ {x y : α}, R x y → R y x)
{a : α}
{l₁ : List α}
{l₂ : List α}
:
List.Pairwise R (l₁ ++ a :: l₂) ↔ List.Pairwise R (a :: (l₁ ++ 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_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_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.filterMap f l)
theorem
List.pairwise_filter
{α : Type u_1}
{R : α → α → Prop}
(p : α → Prop)
[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_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₂ : 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 (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_iff_forall_sublist :
∀ {α : Type u_1} {l : List α} {R : α → α → Prop}, List.Pairwise R l ↔ ∀ {a b : α}, List.Sublist [a, b] l → R a b
@[deprecated List.pairwise_iff_forall_sublist]
theorem
List.pairwise_of_reflexive_on_dupl_of_forall_ne
{α : Type u_1}
[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.map_get_sublist
{α : Type u_1}
{l : List α}
{is : List (Fin (List.length l))}
(h : List.Pairwise (fun (x x_1 : Fin (List.length l)) => ↑x < ↑x_1) is)
:
List.Sublist (List.map (List.get l) is) l
given a list is of monotonically increasing indices into l, getting each index
produces a sublist of l.
theorem
List.sublist_eq_map_get :
∀ {α : Type u_1} {l' l : List α},
List.Sublist l' l →
∃ (is : List (Fin (List.length l))),
l' = List.map (List.get l) is ∧ List.Pairwise (fun (x x_1 : Fin (List.length l)) => x < x_1) is
given a sublist l' <+ l, there exists a list of indices is such that
l' = map (get l) is.
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_replicate
{α : Type u_1}
{r : α → α → Prop}
{x : α}
(hx : r x x)
(n : Nat)
:
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}
[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}
[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_1}
{R : α → α → Prop}
{β : Type u_2}
[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}
[DecidableRel R]
(l : List α)
:
List.Sublist (List.pwFilter R l) l
theorem
List.pwFilter_subset
{α : Type u_1}
{R : α → α → Prop}
[DecidableRel R]
(l : List α)
:
List.pwFilter R l ⊆ l
theorem
List.pairwise_pwFilter
{α : Type u_1}
{R : α → α → Prop}
[DecidableRel R]
(l : List α)
:
List.Pairwise R (List.pwFilter R l)
theorem
List.pwFilter_eq_self
{α : Type u_1}
{R : α → α → Prop}
[DecidableRel R]
{l : List α}
:
List.pwFilter R l = l ↔ List.Pairwise R l
@[simp]
theorem
List.pwFilter_idem
{α : Type u_1}
{R : α → α → Prop}
{l : List α}
[DecidableRel R]
:
List.pwFilter R (List.pwFilter R l) = List.pwFilter R l
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 ∈ List.pwFilter R l → R a b) ↔ ∀ (b : α), b ∈ l → R a b