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 ∀ a ∈ l₁, ∀ b ∈ l₂, r a b, where l₁, l₂ are lists.
@[simp]
theorem
list.forall₂_cons
{α : Type u_1}
{β : Type u_2}
{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_1}
{β : Type u_2}
{R S : α → β → Prop}
(H : ∀ (a : α) (b : β), R a b → S 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 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_1}
{β : Type u_2}
{r : α → β → Prop}
{a : list α}
{b : list β} :
list.forall₂ (flip r) b a → list.forall₂ r a b
theorem
list.forall₂_same
{α : Type u_1}
{r : α → α → Prop}
{l : list α} :
(∀ (x : α), x ∈ l → r x x) → list.forall₂ r l l
theorem
list.forall₂_refl
{α : Type u_1}
{r : α → α → Prop}
[is_refl α r]
(l : list α) :
list.forall₂ r l l
@[simp]
theorem
list.forall₂_nil_left_iff
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
{l : list β} :
list.forall₂ r list.nil l ↔ l = list.nil
@[simp]
theorem
list.forall₂_nil_right_iff
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
{l : list α} :
list.forall₂ r l list.nil ↔ l = list.nil
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₂ (λ (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_1}
{β : Type u_2}
{γ : Type u_3}
{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_1}
{β : Type u_2}
{γ : Type u_3}
{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_1}
{β : Type u_2}
{r : α → β → Prop}
(hr : relator.left_unique r)
{a b : list α}
{c : list β} :
list.forall₂ r a c → list.forall₂ r 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 β} :
list.forall₂ r a b → list.forall₂ r 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 β} :
list.forall₂ R l₁ l₂ → l₁.length = l₂.length
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₂_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₁ 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₁ 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 : relator.bi_unique r) :
(r ⇒ list.forall₂ r ⇒ iff) has_mem.mem has_mem.mem
theorem
list.rel_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{r : α → β → Prop}
{p : γ → δ → Prop} :
((r ⇒ p) ⇒ list.forall₂ r ⇒ list.forall₂ p) list.map list.map
theorem
list.rel_append
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop} :
(list.forall₂ r ⇒ list.forall₂ r ⇒ list.forall₂ r) append append
@[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_bind
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{r : α → β → Prop}
{p : γ → δ → Prop} :
(list.forall₂ r ⇒ (r ⇒ list.forall₂ p) ⇒ list.forall₂ p) 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.forall₂ r ⇒ 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.forall₂ r ⇒ p) list.foldr list.foldr
theorem
list.rel_filter
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
{p : α → Prop}
{q : β → Prop}
[decidable_pred p]
[decidable_pred q]
(hpq : (r ⇒ iff) p q) :
(list.forall₂ r ⇒ list.forall₂ r) (list.filter p) (list.filter q)
theorem
list.rel_filter_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{r : α → β → Prop}
{p : γ → δ → Prop} :
((r ⇒ option.rel p) ⇒ list.forall₂ r ⇒ list.forall₂ p) list.filter_map list.filter_map
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) :
(list.forall₂ r ⇒ r) list.prod list.prod
theorem
list.rel_sum
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
[add_monoid α]
[add_monoid β]
(h : r 0 0)
(hf : (r ⇒ r ⇒ r) has_add.add has_add.add) :
(list.forall₂ r ⇒ r) list.sum list.sum
- nil : ∀ {α : Type u_1} {β : Type u_2} (r : α → β → Prop) {l : list β}, list.sublist_forall₂ r list.nil l
- cons : ∀ {α : Type u_1} {β : Type u_2} (r : α → β → Prop) {a₁ : α} {a₂ : β} {l₁ : list α} {l₂ : list β}, r a₁ a₂ → list.sublist_forall₂ r l₁ l₂ → list.sublist_forall₂ r (a₁ :: l₁) (a₂ :: l₂)
- cons_right : ∀ {α : Type u_1} {β : Type u_2} (r : α → β → Prop) {a : β} {l₁ : list α} {l₂ : list β}, list.sublist_forall₂ r l₁ l₂ → list.sublist_forall₂ r l₁ (a :: l₂)
Given a relation r, sublist_forall₂ r l₁ l₂ indicates that there is a sublist of l₂ such
that forall₂ r l₁ l₂.
theorem
list.sublist_forall₂_iff
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
{l₁ : list α}
{l₂ : list β} :
list.sublist_forall₂ r l₁ l₂ ↔ ∃ (l : list β), list.forall₂ r l₁ l ∧ l <+ l₂
@[protected, instance]
def
list.sublist_forall₂.is_refl
{α : Type u_1}
{ra : α → α → Prop}
[is_refl α ra] :
is_refl (list α) (list.sublist_forall₂ ra)
@[protected, instance]
def
list.sublist_forall₂.is_trans
{α : Type u_1}
{ra : α → α → Prop}
[is_trans α ra] :
is_trans (list α) (list.sublist_forall₂ ra)
theorem
list.sublist.sublist_forall₂
{α : Type u_1}
{l₁ l₂ : list α}
(h : l₁ <+ l₂)
(r : α → α → Prop)
[is_refl α r] :
list.sublist_forall₂ r l₁ l₂
theorem
list.tail_sublist_forall₂_self
{α : Type u_1}
{ra : α → α → Prop}
[is_refl α ra]
(l : list α) :
list.sublist_forall₂ ra l.tail l