# mathlibdocumentation

data.list.forall2

# Double universal quantification on a list #

This file provides an API for list.forall₂ (definition in data.list.defs). forall₂ R l₁ l₂ means that l₁ and l₂ have the same length, and whenever a is the nth element of l₁, and b is the nth element of l₂, then R a b is satisfied.

theorem list.forall₂_iff {α : Type u_1} {β : Type u_2} (R : α → β → Prop) (ᾰ : list α) (ᾰ_1 : list β) :
ᾰ_1 ᾰ_1 = list.nil ∃ {a : α} {b : β} {l₁ : list α} {l₂ : list β}, R a b l₁ l₂ = a :: l₁ ᾰ_1 = b :: l₂
@[simp]
theorem list.forall₂_cons {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {a : α} {b : β} {l₁ : list α} {l₂ : list β} :
(a :: l₁) (b :: l₂) R a b l₁ l₂
theorem list.forall₂.imp {α : Type u_1} {β : Type u_2} {R S : α → β → Prop} (H : ∀ (a : α) (b : β), R a bS a b) {l₁ : list α} {l₂ : list β} (h : l₁ l₂) :
l₁ l₂
theorem list.forall₂.mp {α : Type u_1} {β : Type u_2} {r q s : α → β → Prop} (h : ∀ (a : α) (b : β), r a bq a bs a b) {l₁ : list α} {l₂ : list β} :
l₁ l₂ l₁ l₂ l₁ l₂
theorem list.forall₂.flip {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {a : list α} {b : list β} :
list.forall₂ (flip r) b a a b
@[simp]
theorem list.forall₂_same {α : Type u_1} {r : α → α → Prop} {l : list α} :
l l ∀ (x : α), x lr x x
theorem list.forall₂_refl {α : Type u_1} {r : α → α → Prop} [ r] (l : list α) :
l l
@[simp]
theorem list.forall₂_eq_eq_eq {α : Type u_1} :
@[simp]
theorem list.forall₂_nil_left_iff {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {l : list β} :
@[simp]
theorem list.forall₂_nil_right_iff {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {l : list α} :
theorem list.forall₂_cons_left_iff {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {a : α} {l : list α} {u : list β} :
(a :: l) u ∃ (b : β) (u' : list β), r a b l u' u = b :: u'
theorem list.forall₂_cons_right_iff {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {b : β} {l : list β} {u : list α} :
u (b :: l) ∃ (a : α) (u' : list α), r a b u' l u = a :: u'
theorem list.forall₂_and_left {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {p : α → Prop} (l : list α) (u : list β) :
list.forall₂ (λ (a : α) (b : β), p a r a b) l u (∀ (a : α), a lp a) l u
@[simp]
theorem list.forall₂_map_left_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → β → Prop} {f : γ → α} {l : list γ} {u : list β} :
(list.map f l) u list.forall₂ (λ (c : γ) (b : β), r (f c) b) l u
@[simp]
theorem list.forall₂_map_right_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → β → Prop} {f : γ → β} {l : list α} {u : list γ} :
l (list.map f u) list.forall₂ (λ (a : α) (c : γ), r a (f c)) l u
theorem list.left_unique_forall₂' {α : Type u_1} {β : Type u_2} {r : α → β → Prop} (hr : relator.left_unique r) {a b : list α} {c : list β} :
a c b ca = b
theorem relator.left_unique.forall₂ {α : Type u_1} {β : Type u_2} {r : α → β → Prop} (hr : relator.left_unique r) :
theorem list.right_unique_forall₂' {α : Type u_1} {β : Type u_2} {r : α → β → Prop} (hr : relator.right_unique r) {a : list α} {b c : list β} :
a b a cb = c
theorem relator.right_unique.forall₂ {α : Type u_1} {β : Type u_2} {r : α → β → Prop} (hr : relator.right_unique r) :
theorem relator.bi_unique.forall₂ {α : Type u_1} {β : Type u_2} {r : α → β → Prop} (hr : relator.bi_unique r) :
theorem list.forall₂.length_eq {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {l₁ : list α} {l₂ : list β} :
l₁ l₂l₁.length = l₂.length
theorem list.forall₂.nth_le {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {x : list α} {y : list β} (h : x y) ⦃i : (hx : i < x.length) (hy : i < y.length) :
r (x.nth_le i hx) (y.nth_le i hy)
theorem list.forall₂_of_length_eq_of_nth_le {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {x : list α} {y : list β} :
x.length = y.length(∀ (i : ) (h₁ : i < x.length) (h₂ : i < y.length), r (x.nth_le i h₁) (y.nth_le i h₂)) x y
theorem list.forall₂_iff_nth_le {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {l₁ : list α} {l₂ : list β} :
l₁ l₂ l₁.length = l₂.length ∀ (i : ) (h₁ : i < l₁.length) (h₂ : i < l₂.length), r (l₁.nth_le i h₁) (l₂.nth_le i h₂)
theorem list.forall₂_zip {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {l₁ : list α} {l₂ : list β} :
l₁ l₂∀ {a : α} {b : β}, (a, b) l₁.zip l₂R a b
theorem list.forall₂_iff_zip {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {l₁ : list α} {l₂ : list β} :
l₁ l₂ l₁.length = l₂.length ∀ {a : α} {b : β}, (a, b) l₁.zip l₂R a b
theorem list.forall₂_take {α : Type u_1} {β : Type u_2} {R : α → β → Prop} (n : ) {l₁ : list α} {l₂ : list β} :
l₁ l₂ l₁) l₂)
theorem list.forall₂_drop {α : Type u_1} {β : Type u_2} {R : α → β → Prop} (n : ) {l₁ : list α} {l₂ : list β} :
l₁ l₂ l₁) l₂)
theorem list.forall₂_take_append {α : Type u_1} {β : Type u_2} {R : α → β → Prop} (l : list α) (l₁ l₂ : list β) (h : l (l₁ ++ l₂)) :
(list.take l₁.length l) l₁
theorem list.forall₂_drop_append {α : Type u_1} {β : Type u_2} {R : α → β → Prop} (l : list α) (l₁ l₂ : list β) (h : l (l₁ ++ l₂)) :
(list.drop l₁.length l) l₂
theorem list.rel_mem {α : Type u_1} {β : Type u_2} {r : α → β → Prop} (hr : relator.bi_unique r) :
theorem list.rel_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : α → β → Prop} {p : γ → δ → Prop} :
theorem list.rel_append {α : Type u_1} {β : Type u_2} {r : α → β → Prop} :
theorem list.rel_reverse {α : Type u_1} {β : Type u_2} {r : α → β → Prop} :
@[simp]
theorem list.forall₂_reverse_iff {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {l₁ : list α} {l₂ : list β} :
l₁.reverse l₂.reverse l₁ l₂
theorem list.rel_join {α : Type u_1} {β : Type u_2} {r : α → β → Prop} :
theorem list.rel_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : α → β → Prop} {p : γ → δ → Prop} :
theorem list.rel_foldl {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : α → β → Prop} {p : γ → δ → Prop} :
theorem list.rel_foldr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : α → β → Prop} {p : γ → δ → Prop} :
theorem list.rel_filter {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {p : α → Prop} {q : β → Prop} (hpq : (r iff) p q) :
theorem list.rel_filter_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : α → β → Prop} {p : γ → δ → Prop} :
theorem list.rel_prod {α : Type u_1} {β : Type u_2} {r : α → β → Prop} [monoid α] [monoid β] (h : r 1 1) (hf : (r r r) has_mul.mul has_mul.mul) :
theorem list.rel_sum {α : Type u_1} {β : Type u_2} {r : α → β → Prop} [add_monoid α] [add_monoid β] (h : r 0 0) (hf : (r r r) has_add.add has_add.add) :
inductive list.sublist_forall₂ {α : Type u_1} {β : Type u_2} (r : α → β → Prop) :
list αlist β → Prop
• nil : ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {l : list β},
• cons : ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {a₁ : α} {a₂ : β} {l₁ : list α} {l₂ : list β}, r a₁ a₂ l₂ (a₁ :: l₁) (a₂ :: l₂)
• cons_right : ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {a : β} {l₁ : list α} {l₂ : list β}, l₂ (a :: l₂)

Given a relation r, sublist_forall₂ r l₁ l₂ indicates that there is a sublist of l₂ such that forall₂ r l₁ l₂.

Instances for list.sublist_forall₂
theorem list.sublist_forall₂_iff {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {l₁ : list α} {l₂ : list β} :
l₂ ∃ (l : list β), l₁ l l <+ l₂
@[protected, instance]
def list.sublist_forall₂.is_refl {α : Type u_1} {ra : α → α → Prop} [ ra] :
@[protected, instance]
def list.sublist_forall₂.is_trans {α : Type u_1} {ra : α → α → Prop} [ ra] :
theorem list.sublist.sublist_forall₂ {α : Type u_1} {l₁ l₂ : list α} (h : l₁ <+ l₂) (r : α → α → Prop) [ r] :
l₂
theorem list.tail_sublist_forall₂_self {α : Type u_1} {ra : α → α → Prop} [ ra] (l : list α) :
l