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✝¹ : List β) : Forall₂ R a✝ a✝¹ ↔ a✝ = [] ∧ a✝¹ = [] ∨ ∃ (a : α), ∃ (b : β), ∃ (l₁ : List α), ∃ (l₂ : List β), R a b ∧ Forall₂ R l₁ l₂ ∧ a✝ = a :: l₁ ∧ a✝¹ = b :: 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 : Forall₂ R l₁ l₂) : Forall₂ S 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 β} : Forall₂ Q l₁ l₂ → Forall₂ R l₁ l₂ → Forall₂ S l₁ l₂

theorem List.Forall₂.flip {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {a : List α} {b : List β} : Forall₂ (_root_.flip R) b a → Forall₂ R a b

@[simp]

theorem List.forall₂_same {α : Type u_1} {Rₐ : α → α → Prop} {l : List α} : Forall₂ Rₐ l l ↔ ∀ (x : α), x ∈ l → Rₐ x x

theorem List.forall₂_refl {α : Type u_1} {Rₐ : α → α → Prop} [IsRefl α Rₐ] (l : List α) : Forall₂ Rₐ l l

@[simp]

theorem List.forall₂_eq_eq_eq {α : Type u_1} : (Forall₂ fun (x1 x2 : α) => x1 = x2) = Eq

@[simp]

theorem List.forall₂_nil_left_iff {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {l : List β} : Forall₂ R [] l ↔ l = []

@[simp]

theorem List.forall₂_nil_right_iff {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {l : List α} : Forall₂ R l [] ↔ l = []

theorem List.forall₂_cons_left_iff {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {a : α} {l : List α} {u : List β} : Forall₂ R (a :: l) u ↔ ∃ (b : β), ∃ (u' : List β), R a b ∧ 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 α} : Forall₂ R u (b :: l) ↔ ∃ (a : α), ∃ (u' : List α), R a b ∧ 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 β) : Forall₂ (fun (a : α) (b : β) => p a ∧ R a b) l u ↔ (∀ (a : α), a ∈ l → p a) ∧ 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 β} : Forall₂ R (map f l) u ↔ 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 γ} : Forall₂ R l (map f u) ↔ Forall₂ (fun (a : α) (c : γ) => R a (f c)) l u

theorem List.left_unique_forall₂' {α : Type u_1} {β : Type u_2} {R : α → β → Prop} (hr : Relator.LeftUnique R) {a b : List α} {c : List β} : Forall₂ R a c → Forall₂ R b c → a = b

theorem Relator.LeftUnique.forall₂ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} (hr : LeftUnique R) : LeftUnique (List.Forall₂ R)

theorem List.right_unique_forall₂' {α : Type u_1} {β : Type u_2} {R : α → β → Prop} (hr : Relator.RightUnique R) {a : List α} {b c : List β} : Forall₂ R a b → Forall₂ R a c → b = c

theorem Relator.RightUnique.forall₂ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} (hr : RightUnique R) : RightUnique (List.Forall₂ R)

theorem Relator.BiUnique.forall₂ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} (hr : BiUnique R) : BiUnique (List.Forall₂ R)

theorem List.Forall₂.length_eq {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {l₁ : List α} {l₂ : 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 β} : Forall₂ R x y → ∀ ⦃i : ℕ⦄ (hx : i < x.length) (hy : i < y.length), R (x.get ⟨i, hx⟩) (y.get ⟨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₂⟩)) → Forall₂ R x y

theorem List.forall₂_iff_get {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {l₁ : List α} {l₂ : 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₂⟩)

theorem List.forall₂_zip {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {l₁ : List α} {l₂ : 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 β} : 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 β} : Forall₂ R l₁ l₂ → Forall₂ R (take n l₁) (take n l₂)

theorem List.forall₂_drop {α : Type u_1} {β : Type u_2} {R : α → β → Prop} (n : ℕ) {l₁ : List α} {l₂ : List β} : Forall₂ R l₁ l₂ → Forall₂ R (drop n l₁) (drop n l₂)

theorem List.forall₂_take_append {α : Type u_1} {β : Type u_2} {R : α → β → Prop} (l : List α) (l₁ l₂ : List β) (h : Forall₂ R l (l₁ ++ l₂)) : Forall₂ R (take l₁.length l) l₁

theorem List.forall₂_drop_append {α : Type u_1} {β : Type u_2} {R : α → β → Prop} (l : List α) (l₁ l₂ : List β) (h : Forall₂ R l (l₁ ++ l₂)) : Forall₂ R (drop l₁.length l) l₂

theorem List.rel_mem {α : Type u_1} {β : Type u_2} {R : α → β → Prop} (hr : Relator.BiUnique R) : (R ⇒ Forall₂ R ⇒ Iff) (fun (x1 : α) (x2 : List α) => x1 ∈ x2) fun (x1 : β) (x2 : List β) => x1 ∈ x2

theorem List.rel_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {R : α → β → Prop} {P : γ → δ → Prop} : ((R ⇒ P) ⇒ Forall₂ R ⇒ Forall₂ P) map map

theorem List.rel_append {α : Type u_1} {β : Type u_2} {R : α → β → Prop} : (Forall₂ R ⇒ Forall₂ R ⇒ Forall₂ R) (fun (x1 x2 : List α) => x1 ++ x2) fun (x1 x2 : List β) => x1 ++ x2

theorem List.rel_reverse {α : Type u_1} {β : Type u_2} {R : α → β → Prop} : (Forall₂ R ⇒ Forall₂ R) reverse reverse

@[simp]

theorem List.forall₂_reverse_iff {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {l₁ : List α} {l₂ : List β} : Forall₂ R l₁.reverse l₂.reverse ↔ Forall₂ R l₁ l₂

theorem List.rel_flatten {α : Type u_1} {β : Type u_2} {R : α → β → Prop} : (Forall₂ (Forall₂ R) ⇒ Forall₂ R) flatten flatten

@[deprecated List.rel_flatten (since := "2025-10-15")]

theorem List.rel_join {α : Type u_1} {β : Type u_2} {R : α → β → Prop} : (Forall₂ (Forall₂ R) ⇒ Forall₂ R) flatten flatten

Alias of List.rel_flatten.

theorem List.rel_flatMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {R : α → β → Prop} {P : γ → δ → Prop} : (Forall₂ R ⇒ (R ⇒ Forall₂ P) ⇒ Forall₂ P) (Function.swap flatMap) (Function.swap flatMap)

@[deprecated List.rel_flatMap (since := "2025-10-16")]

theorem List.rel_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {R : α → β → Prop} {P : γ → δ → Prop} : (Forall₂ R ⇒ (R ⇒ Forall₂ P) ⇒ Forall₂ P) (Function.swap flatMap) (Function.swap flatMap)

Alias of List.rel_flatMap.

theorem List.rel_foldl {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {R : α → β → Prop} {P : γ → δ → Prop} : ((P ⇒ R ⇒ P) ⇒ P ⇒ Forall₂ R ⇒ P) foldl 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 ⇒ Forall₂ R ⇒ P) foldr foldr

theorem List.rel_filter {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {p : α → Bool} {q : β → Bool} (hpq : (R ⇒ fun (x1 x2 : Prop) => x1 ↔ x2) (fun (x : α) => p x = true) fun (x : β) => q x = true) : (Forall₂ R ⇒ Forall₂ R) (filter p) (filter q)

theorem List.rel_filterMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {R : α → β → Prop} {P : γ → δ → Prop} : ((R ⇒ Option.Rel P) ⇒ Forall₂ R ⇒ Forall₂ P) filterMap 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₂.

• nil {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {l : List β} : SublistForall₂ R [] l
• cons {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {a₁ : α} {a₂ : β} {l₁ : List α} {l₂ : List β} : R a₁ a₂ → SublistForall₂ R l₁ l₂ → SublistForall₂ R (a₁ :: l₁) (a₂ :: l₂)
• cons_right {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {a : β} {l₁ : List α} {l₂ : List β} : SublistForall₂ R l₁ l₂ → SublistForall₂ R l₁ (a :: l₂)

theorem List.sublistForall₂_iff {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {l₁ : List α} {l₂ : List β} : SublistForall₂ R l₁ l₂ ↔ ∃ (l : List β), Forall₂ R l₁ l ∧ l.Sublist l₂

instance List.SublistForall₂.is_refl {α : Type u_1} {Rₐ : α → α → Prop} [IsRefl α Rₐ] : IsRefl (List α) (SublistForall₂ Rₐ)

instance List.SublistForall₂.is_trans {α : Type u_1} {Rₐ : α → α → Prop} [IsTrans α Rₐ] : IsTrans (List α) (SublistForall₂ Rₐ)

theorem List.Sublist.sublistForall₂ {α : Type u_1} {Rₐ : α → α → Prop} {l₁ l₂ : List α} (h : l₁.Sublist l₂) [IsRefl α Rₐ] : SublistForall₂ Rₐ l₁ l₂

theorem List.tail_sublistForall₂_self {α : Type u_1} {Rₐ : α → α → Prop} [IsRefl α Rₐ] (l : List α) : SublistForall₂ Rₐ l.tail l

@[simp]

theorem List.sublistForall₂_map_left_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R : α → β → Prop} {f : γ → α} {l₁ : List γ} {l₂ : List β} : SublistForall₂ R (map f l₁) l₂ ↔ SublistForall₂ (fun (c : γ) (b : β) => R (f c) b) l₁ l₂

@[simp]

theorem List.sublistForall₂_map_right_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R : α → β → Prop} {f : γ → β} {l₁ : List α} {l₂ : List γ} : SublistForall₂ R l₁ (map f l₂) ↔ SublistForall₂ (fun (a : α) (c : γ) => R a (f c)) l₁ l₂