Double universal quantification on a list #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
@[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 S Q : α → β → Prop}
(h : ∀ (a : α) (b : β), Q a b → R a b → S 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 β} :
list.forall₂ (flip R) b a → list.forall₂ R a b
theorem
list.forall₂_refl
{α : Type u_1}
{Rₐ : α → α → Prop}
[is_refl α Rₐ]
(l : list α) :
list.forall₂ Rₐ l l
@[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₂_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
@[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₂.
Instances for list.sublist_forall₂
@[protected, instance]
def
list.sublist_forall₂.is_refl
{α : Type u_1}
{Rₐ : α → α → Prop}
[is_refl α Rₐ] :
is_refl (list α) (list.sublist_forall₂ Rₐ)
@[protected, instance]
def
list.sublist_forall₂.is_trans
{α : Type u_1}
{Rₐ : α → α → Prop}
[is_trans α Rₐ] :
is_trans (list α) (list.sublist_forall₂ Rₐ)
theorem
list.sublist.sublist_forall₂
{α : Type u_1}
{Rₐ : α → α → Prop}
{l₁ l₂ : list α}
(h : l₁ <+ l₂)
[is_refl α Rₐ] :
list.sublist_forall₂ Rₐ l₁ l₂
theorem
list.tail_sublist_forall₂_self
{α : Type u_1}
{Rₐ : α → α → Prop}
[is_refl α Rₐ]
(l : list α) :
list.sublist_forall₂ Rₐ l.tail l