@[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 b → S 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 b → q a b → s 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 β} :
list.forall₂ (flip r) b a → list.forall₂ r a b
theorem
list.forall₂_same
{α : Type u}
{r : α → α → Prop}
{l : list α} :
(∀ (x : α), x ∈ l → r x x) → list.forall₂ r l l
theorem
list.forall₂_refl
{α : Type u}
{r : α → α → Prop}
[is_refl α r]
(l : list α) :
list.forall₂ r l l
@[simp]
theorem
list.forall₂_nil_left_iff
{α : Type u}
{β : Type v}
{r : α → β → Prop}
{l : list β} :
list.forall₂ r list.nil l ↔ l = list.nil
@[simp]
theorem
list.forall₂_nil_right_iff
{α : Type u}
{β : Type v}
{r : α → β → Prop}
{l : list α} :
list.forall₂ r l list.nil ↔ l = list.nil
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 ∈ l → p 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.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 : β} :
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} :
relator.bi_unique r → (r ⇒ list.forall₂ r ⇒ iff) has_mem.mem has_mem.mem
theorem
list.rel_map
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type z}
{r : α → β → Prop}
{p : γ → δ → Prop} :
((r ⇒ p) ⇒ list.forall₂ r ⇒ list.forall₂ p) list.map list.map
theorem
list.rel_bind
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type z}
{r : α → β → Prop}
{p : γ → δ → Prop} :
(list.forall₂ r ⇒ (r ⇒ list.forall₂ p) ⇒ list.forall₂ p) list.bind list.bind
theorem
list.rel_foldl
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type z}
{r : α → β → Prop}
{p : γ → δ → Prop} :
((p ⇒ r ⇒ p) ⇒ p ⇒ list.forall₂ r ⇒ p) list.foldl list.foldl
theorem
list.rel_foldr
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type z}
{r : α → β → Prop}
{p : γ → δ → Prop} :
((r ⇒ p ⇒ p) ⇒ p ⇒ list.forall₂ r ⇒ p) list.foldr list.foldr
theorem
list.rel_filter
{α : Type u}
{β : Type v}
{r : α → β → Prop}
{p : α → Prop}
{q : β → Prop}
[decidable_pred p]
[decidable_pred q] :
(r ⇒ iff) p q → (list.forall₂ r ⇒ list.forall₂ r) (list.filter p) (list.filter 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} :
((r ⇒ option.rel p) ⇒ list.forall₂ r ⇒ list.forall₂ p) list.filter_map list.filter_map
theorem
list.rel_sum
{α : Type u}
{β : Type v}
{r : α → β → Prop}
[add_monoid α]
[add_monoid β] :
r 0 0 → (r ⇒ r ⇒ r) has_add.add has_add.add → (list.forall₂ r ⇒ r) list.sum list.sum
theorem
list.rel_prod
{α : Type u}
{β : Type v}
{r : α → β → Prop}
[monoid α]
[monoid β] :
r 1 1 → (r ⇒ r ⇒ r) has_mul.mul has_mul.mul → (list.forall₂ r ⇒ r) list.prod list.prod