# mathlib3documentation

data.list.forall2

# Double universal quantification on a list #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 b S a b) {l₁ : list α} {l₂ : list β} (h : l₁ l₂) :
l₁ l₂
theorem list.forall₂.mp {α : Type u_1} {β : Type u_2} {R S Q : α β Prop} (h : (a : α) (b : β), Q a b R a b S 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 l Rₐ 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 l p 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 c a = 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 c b = 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) :
inductive list.sublist_forall₂ {α : Type u_1} {β : Type u_2} (R : α β Prop) :
list α list β Prop

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} {Rₐ : α α Prop} [ Rₐ] :
@[protected, instance]
def list.sublist_forall₂.is_trans {α : Type u_1} {Rₐ : α α Prop} [ Rₐ] :
theorem list.sublist.sublist_forall₂ {α : Type u_1} {Rₐ : α α Prop} {l₁ l₂ : list α} (h : l₁ <+ l₂) [ Rₐ] :
l₁ l₂
theorem list.tail_sublist_forall₂_self {α : Type u_1} {Rₐ : α α Prop} [ Rₐ] (l : list α) :
l