theorem
list.rel_of_pairwise_cons
{α : Type u}
{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}
{R : α → α → Prop}
{a : α}
{l : list α} :
list.pairwise R (a :: l) → list.pairwise R l
theorem
list.pairwise.imp_of_mem
{α : Type u}
{R S : α → α → Prop}
{l : list α} :
(∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → list.pairwise R l → list.pairwise S l
theorem
list.pairwise.imp
{α : Type u}
{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}
{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}
{R S T : α → α → Prop}
(H : ∀ (a b : α), R a b → S a b → T a b)
{l : list α} :
list.pairwise R l → list.pairwise S l → list.pairwise T l
theorem
list.pairwise.iff_of_mem
{α : Type u}
{R S : α → α → Prop}
{l : list α} :
(∀ {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}
{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}
{R : α → α → Prop}
{l : list α} :
(∀ (x y : α), R x y) → list.pairwise R l
theorem
list.pairwise.and_mem
{α : Type u}
{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}
{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}
{R : α → α → Prop}
{l₁ l₂ : list α} :
l₁ <+ l₂ → list.pairwise R l₂ → list.pairwise R l₁
theorem
list.forall_of_forall_of_pairwise
{α : Type u}
{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 : α) :
y ∈ l → R x y
theorem
list.forall_of_pairwise
{α : Type u}
{R : α → α → Prop}
(H : symmetric R)
{l : list α}
(hl : list.pairwise R l)
(a : α)
(H_1 : a ∈ l)
(b : α) :
theorem
list.pairwise_pair
{α : Type u}
{R : α → α → Prop}
{a b : α} :
list.pairwise R [a, b] ↔ R a b
theorem
list.pairwise_append
{α : Type u}
{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}
{R : α → α → Prop}
(s : symmetric R)
{l₁ l₂ : list α} :
list.pairwise R (l₁ ++ l₂) ↔ list.pairwise R (l₂ ++ l₁)
theorem
list.pairwise_middle
{α : Type u}
{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}
{β : Type v}
{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}
{β : Type v}
{R : α → α → Prop}
{S : β → β → Prop}
(f : α → β)
(H : ∀ (a b : α), S (f a) (f b) → R a b)
{l : list α} :
list.pairwise S (list.map f l) → list.pairwise R l
theorem
list.pairwise_map_of_pairwise
{α : Type u}
{β : Type v}
{R : α → α → Prop}
{S : β → β → Prop}
(f : α → β)
(H : ∀ (a b : α), R a b → S (f a) (f b))
{l : list α} :
list.pairwise R l → list.pairwise S (list.map f l)
theorem
list.pairwise_filter_map
{α : Type u}
{β : Type v}
{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}
{β : Type v}
{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 α} :
list.pairwise R l → list.pairwise S (list.filter_map f l)
theorem
list.pairwise_filter
{α : Type u}
{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}
{R : α → α → Prop}
(p : α → Prop)
[decidable_pred p]
{l : list α} :
list.pairwise R l → list.pairwise R (list.filter p l)
theorem
list.pairwise_join
{α : Type u}
{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}
{R : α → α → Prop}
{l : list α} :
list.pairwise R l.reverse ↔ list.pairwise (λ (x y : α), R y x) l
theorem
list.pairwise_sublists'
{α : Type u}
{R : α → α → Prop}
{l : list α} :
list.pairwise R l → list.pairwise (list.lex (function.swap R)) l.sublists'
theorem
list.pairwise_sublists
{α : Type u}
{R : α → α → Prop}
{l : list α} :
list.pairwise R l → list.pairwise (λ (l₁ l₂ : list α), list.lex R l₁.reverse l₂.reverse) l.sublists
@[simp]
@[simp]
theorem
list.pw_filter_cons_of_pos
{α : Type u}
{R : α → α → Prop}
[decidable_rel R]
{a : α}
{l : list α} :
(∀ (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}
{R : α → α → Prop}
[decidable_rel R]
{a : α}
{l : list α} :
(¬∀ (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}
{β : Type v}
{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}
{R : α → α → Prop}
[decidable_rel R]
(l : list α) :
list.pw_filter R l <+ l
theorem
list.pw_filter_subset
{α : Type u}
{R : α → α → Prop}
[decidable_rel R]
(l : list α) :
list.pw_filter R l ⊆ l
theorem
list.pairwise_pw_filter
{α : Type u}
{R : α → α → Prop}
[decidable_rel R]
(l : list α) :
list.pairwise R (list.pw_filter R l)
theorem
list.pw_filter_eq_self
{α : Type u}
{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}
{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}
{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