mathlib documentation

data.list.forall2

@[simp]
theorem list.forall₂_cons {α : Type u} {β : Type v} {R : α → β → Prop} {a : α} {b : β} {l₁ : list α} {l₂ : list β} :
list.forall₂ R (a :: l₁) (b :: l₂) R a b list.forall₂ R l₁ l₂

theorem list.forall₂.imp {α : Type u} {β : Type v} {R S : α → β → Prop} (H : ∀ (a : α) (b : β), R a bS a b) {l₁ : list α} {l₂ : list β} :
list.forall₂ R l₁ l₂list.forall₂ S l₁ l₂

theorem list.forall₂.mp {α : Type u} {β : Type v} {r q s : α → β → Prop} (h : ∀ (a : α) (b : β), r a bq a bs a b) {l₁ : list α} {l₂ : list β} :
list.forall₂ r l₁ l₂list.forall₂ q l₁ l₂list.forall₂ s l₁ l₂

theorem list.forall₂.flip {α : Type u} {β : Type v} {r : α → β → Prop} {a : list α} {b : list β} :

theorem list.forall₂_same {α : Type u} {r : α → α → Prop} {l : list α} :
(∀ (x : α), x lr x x)list.forall₂ r l l

theorem list.forall₂_refl {α : Type u} {r : α → α → Prop} [is_refl α r] (l : list α) :

theorem list.forall₂_eq_eq_eq {α : Type u} :

@[simp]
theorem list.forall₂_nil_left_iff {α : Type u} {β : Type v} {r : α → β → Prop} {l : list β} :

@[simp]
theorem list.forall₂_nil_right_iff {α : Type u} {β : Type v} {r : α → β → Prop} {l : list α} :

theorem list.forall₂_cons_left_iff {α : Type u} {β : Type v} {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} {β : Type v} {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} {β : Type v} {r : α → β → Prop} {p : α → Prop} (l : list α) (u : list β) :
list.forall₂ (λ (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} {β : Type v} {γ : Type w} {r : α → β → Prop} {f : γ → α} {l : list γ} {u : list β} :
list.forall₂ r (list.map f l) u list.forall₂ (λ (c : γ) (b : β), r (f c) b) l u

@[simp]
theorem list.forall₂_map_right_iff {α : Type u} {β : Type v} {γ : Type w} {r : α → β → Prop} {f : γ → β} {l : list α} {u : list γ} :
list.forall₂ r l (list.map f u) list.forall₂ (λ (a : α) (c : γ), r a (f c)) l u

theorem list.left_unique_forall₂ {α : Type u} {β : Type v} {r : α → β → Prop} :

theorem list.right_unique_forall₂ {α : Type u} {β : Type v} {r : α → β → Prop} :

theorem list.bi_unique_forall₂ {α : Type u} {β : Type v} {r : α → β → Prop} :

theorem list.forall₂_length_eq {α : Type u} {β : Type v} {R : α → β → Prop} {l₁ : list α} {l₂ : list β} :
list.forall₂ R l₁ l₂l₁.length = l₂.length

theorem list.forall₂_zip {α : Type u} {β : Type v} {R : α → β → Prop} {l₁ : list α} {l₂ : list β} (a : list.forall₂ R l₁ l₂) {a_1 : α} {b : β} :
(a_1, b) l₁.zip l₂R a_1 b

theorem list.forall₂_iff_zip {α : Type u} {β : Type v} {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} {β : Type v} {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} {β : Type v} {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} {β : Type v} {R : α → β → Prop} (l : list α) (l₁ l₂ : list β) :
list.forall₂ R l (l₁ ++ l₂)list.forall₂ R (list.take l₁.length l) l₁

theorem list.forall₂_drop_append {α : Type u} {β : Type v} {R : α → β → Prop} (l : list α) (l₁ l₂ : list β) :
list.forall₂ R l (l₁ ++ l₂)list.forall₂ R (list.drop l₁.length l) l₂

theorem list.rel_mem {α : Type u} {β : Type v} {r : α → β → Prop} :

theorem list.rel_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type z} {r : α → β → Prop} {p : γ → δ → Prop} :

theorem list.rel_append {α : Type u} {β : Type v} {r : α → β → Prop} :

theorem list.rel_join {α : Type u} {β : Type v} {r : α → β → Prop} :

theorem list.rel_bind {α : Type u} {β : Type v} {γ : Type w} {δ : Type z} {r : α → β → Prop} {p : γ → δ → Prop} :

theorem list.rel_foldl {α : Type u} {β : Type v} {γ : Type w} {δ : Type z} {r : α → β → Prop} {p : γ → δ → Prop} :

theorem list.rel_foldr {α : Type u} {β : Type v} {γ : Type w} {δ : Type z} {r : α → β → Prop} {p : γ → δ → Prop} :

theorem list.rel_filter {α : Type u} {β : Type v} {r : α → β → Prop} {p : α → Prop} {q : β → Prop} [decidable_pred p] [decidable_pred q] :

theorem list.filter_map_cons {α : Type u} {β : Type v} (f : α → option β) (a : α) (l : list α) :
list.filter_map f (a :: l) = (f a).cases_on (list.filter_map f l) (λ (b : β), b :: list.filter_map f l)

theorem list.rel_filter_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type z} {r : α → β → Prop} {p : γ → δ → Prop} :

theorem list.rel_prod {α : Type u} {β : Type v} {r : α → β → Prop} [monoid α] [monoid β] :

theorem list.rel_sum {α : Type u} {β : Type v} {r : α → β → Prop} [add_monoid α] [add_monoid β] :