# 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) :
∀ (a : List α) (a_1 : List β), List.Forall₂ R a a_1 a = [] a_1 = [] ∃ (a_2 : α), ∃ (b : β), ∃ (l₁ : List α), ∃ (l₂ : List β), R a_2 b List.Forall₂ R l₁ l₂ a = a_2 :: l₁ a_1 = b :: l₂
theorem List.Forall₂.imp {α : Type u_1} {β : Type u_2} {R : αβProp} {S : αβProp} (H : ∀ (a : α) (b : β), R a bS a b) {l₁ : List α} {l₂ : List β} (h : List.Forall₂ R l₁ l₂) :
List.Forall₂ S l₁ l₂
theorem List.Forall₂.mp {α : Type u_1} {β : Type u_2} {R : αβProp} {S : αβProp} {Q : αβProp} (h : ∀ (a : α) (b : β), Q a bR a bS a b) {l₁ : List α} {l₂ : List β} :
List.Forall₂ Q l₁ l₂List.Forall₂ R l₁ l₂List.Forall₂ S l₁ l₂
theorem List.Forall₂.flip {α : Type u_1} {β : Type u_2} {R : αβProp} {a : List α} {b : List β} :
@[simp]
theorem List.forall₂_same {α : Type u_1} {Rₐ : ααProp} {l : List α} :
List.Forall₂ Rₐ l l ∀ (x : α), x lRₐ x x
theorem List.forall₂_refl {α : Type u_1} {Rₐ : ααProp} [IsRefl α Rₐ] (l : List α) :
@[simp]
theorem List.forall₂_eq_eq_eq {α : Type u_1} :
(List.Forall₂ fun (x x_1 : α) => x = x_1) = Eq
@[simp]
theorem List.forall₂_nil_left_iff {α : Type u_1} {β : Type u_2} {R : αβProp} {l : List β} :
List.Forall₂ R [] l l = []
@[simp]
theorem List.forall₂_nil_right_iff {α : Type u_1} {β : Type u_2} {R : αβProp} {l : List α} :
List.Forall₂ R l [] l = []
theorem List.forall₂_cons_left_iff {α : Type u_1} {β : Type u_2} {R : αβProp} {a : α} {l : List α} {u : List β} :
List.Forall₂ R (a :: l) u ∃ (b : β), ∃ (u' : List β), R a b List.Forall₂ R l u' u = b :: u'
theorem List.forall₂_cons_right_iff {α : Type u_1} {β : Type u_2} {R : αβProp} {b : β} {l : List β} {u : List α} :
List.Forall₂ R u (b :: l) ∃ (a : α), ∃ (u' : List α), R a b List.Forall₂ R 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₂ (fun (a : α) (b : β) => p a R a b) l u (∀ (a : α), a lp a) List.Forall₂ R 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.Forall₂ R (List.map f l) u List.Forall₂ (fun (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 γ} :
List.Forall₂ R l (List.map f u) List.Forall₂ (fun (a : α) (c : γ) => R a (f c)) l u
theorem List.left_unique_forall₂' {α : Type u_1} {β : Type u_2} {R : αβProp} (hr : ) {a : List α} {b : List α} {c : List β} :
List.Forall₂ R a cList.Forall₂ R b ca = b
theorem Relator.LeftUnique.forall₂ {α : Type u_1} {β : Type u_2} {R : αβProp} (hr : ) :
theorem List.right_unique_forall₂' {α : Type u_1} {β : Type u_2} {R : αβProp} (hr : ) {a : List α} {b : List β} {c : List β} :
List.Forall₂ R a bList.Forall₂ R a cb = c
theorem Relator.RightUnique.forall₂ {α : Type u_1} {β : Type u_2} {R : αβProp} (hr : ) :
theorem Relator.BiUnique.forall₂ {α : Type u_1} {β : Type u_2} {R : αβProp} (hr : ) :
theorem List.Forall₂.length_eq {α : Type u_1} {β : Type u_2} {R : αβProp} {l₁ : List α} {l₂ : List β} :
List.Forall₂ R l₁ l₂l₁.length = l₂.length
theorem List.Forall₂.get {α : Type u_1} {β : Type u_2} {R : αβProp} {x : List α} {y : List β} :
List.Forall₂ R x y∀ ⦃i : ⦄ (hx : i < x.length) (hy : i < y.length), R (x.get i, hx) (y.get i, hy)
@[deprecated]
theorem List.Forall₂.nthLe {α : Type u_1} {β : Type u_2} {R : αβProp} {x : List α} {y : List β} (h : List.Forall₂ R x y) ⦃i : (hx : i < x.length) (hy : i < y.length) :
R (x.nthLe i hx) (y.nthLe i hy)
theorem List.forall₂_of_length_eq_of_get {α : 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.get i, h₁) (y.get i, h₂))List.Forall₂ R x y
@[deprecated]
theorem List.forall₂_of_length_eq_of_nthLe {α : Type u_1} {β : Type u_2} {R : αβProp} {x : List α} {y : List β} (H : x.length = y.length) (H' : ∀ (i : ) (h₁ : i < x.length) (h₂ : i < y.length), R (x.nthLe i h₁) (y.nthLe i h₂)) :
theorem List.forall₂_iff_get {α : Type u_1} {β : Type u_2} {R : αβProp} {l₁ : List α} {l₂ : List β} :
List.Forall₂ R l₁ l₂ l₁.length = l₂.length ∀ (i : ) (h₁ : i < l₁.length) (h₂ : i < l₂.length), R (l₁.get i, h₁) (l₂.get i, h₂)
@[deprecated]
theorem List.forall₂_iff_nthLe {α : Type u_1} {β : Type u_2} {R : αβProp} {l₁ : List α} {l₂ : List β} :
List.Forall₂ R l₁ l₂ l₁.length = l₂.length ∀ (i : ) (h₁ : i < l₁.length) (h₂ : i < l₂.length), R (l₁.nthLe i h₁) (l₂.nthLe i h₂)
theorem List.forall₂_zip {α : Type u_1} {β : Type u_2} {R : αβProp} {l₁ : List α} {l₂ : List β} :
List.Forall₂ R 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 β} :
List.Forall₂ R 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 β} :
List.Forall₂ R l₁ l₂List.Forall₂ R (List.take n l₁) (List.take n l₂)
theorem List.forall₂_drop {α : Type u_1} {β : Type u_2} {R : αβProp} (n : ) {l₁ : List α} {l₂ : List β} :
List.Forall₂ R l₁ l₂List.Forall₂ R (List.drop n l₁) (List.drop n l₂)
theorem List.forall₂_take_append {α : Type u_1} {β : Type u_2} {R : αβProp} (l : List α) (l₁ : List β) (l₂ : List β) (h : List.Forall₂ R l (l₁ ++ l₂)) :
List.Forall₂ R (List.take l₁.length l) l₁
theorem List.forall₂_drop_append {α : Type u_1} {β : Type u_2} {R : αβProp} (l : List α) (l₁ : List β) (l₂ : List β) (h : List.Forall₂ R l (l₁ ++ l₂)) :
List.Forall₂ R (List.drop l₁.length l) l₂
theorem List.rel_mem {α : Type u_1} {β : Type u_2} {R : αβProp} (hr : ) :
(R ) (fun (x : α) (x_1 : List α) => x x_1) fun (x : β) (x_1 : List β) => x x_1
theorem List.rel_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {R : αβProp} {P : γδProp} :
((R P) ) List.map List.map
theorem List.rel_append {α : Type u_1} {β : Type u_2} {R : αβProp} :
() (fun (x x_1 : List α) => x ++ x_1) fun (x x_1 : List β) => x ++ x_1
theorem List.rel_reverse {α : Type u_1} {β : Type u_2} {R : αβProp} :
() List.reverse List.reverse
@[simp]
theorem List.forall₂_reverse_iff {α : Type u_1} {β : Type u_2} {R : αβProp} {l₁ : List α} {l₂ : List β} :
List.Forall₂ R l₁.reverse l₂.reverse List.Forall₂ R l₁ l₂
theorem List.rel_join {α : Type u_1} {β : Type u_2} {R : αβProp} :
() List.join List.join
theorem List.rel_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {R : αβProp} {P : γδProp} :
( () ) List.bind List.bind
theorem List.rel_foldl {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {R : αβProp} {P : γδProp} :
((P R P) P ) List.foldl List.foldl
theorem List.rel_foldr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {R : αβProp} {P : γδProp} :
((R P P) P ) List.foldr List.foldr
theorem List.rel_filter {α : Type u_1} {β : Type u_2} {R : αβProp} {p : αBool} {q : βBool} (hpq : (R fun (x x_1 : Prop) => x x_1) (fun (x : α) => p x = true) fun (x : β) => q x = true) :
() () ()
theorem List.rel_filterMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {R : αβProp} {P : γδProp} :
((R ) ) List.filterMap List.filterMap
inductive List.SublistForall₂ {α : 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
theorem List.sublistForall₂_iff {α : Type u_1} {β : Type u_2} {R : αβProp} {l₁ : List α} {l₂ : List β} :
List.SublistForall₂ R l₁ l₂ ∃ (l : List β), List.Forall₂ R l₁ l l.Sublist l₂
instance List.SublistForall₂.is_refl {α : Type u_1} {Rₐ : ααProp} [IsRefl α Rₐ] :
IsRefl (List α) ()
Equations
• =
instance List.SublistForall₂.is_trans {α : Type u_1} {Rₐ : ααProp} [IsTrans α Rₐ] :
IsTrans (List α) ()
Equations
• =
theorem List.Sublist.sublistForall₂ {α : Type u_1} {Rₐ : ααProp} {l₁ : List α} {l₂ : List α} (h : l₁.Sublist l₂) [IsRefl α Rₐ] :
List.SublistForall₂ Rₐ l₁ l₂
theorem List.tail_sublistForall₂_self {α : Type u_1} {Rₐ : ααProp} [IsRefl α Rₐ] (l : List α) :
List.SublistForall₂ Rₐ l.tail l