Forall2

📁 Source: Mathlib/Data/List/Forall2.lean

Statistics

Metric	Count
Definitions SublistForall₂	1
Theorems flip, get, imp, length_eq, mp, sublistForall₂, is_refl, is_trans, forall₂_and_left, forall₂_cons_left_iff, forall₂_cons_right_iff, forall₂_drop, forall₂_drop_append, forall₂_eq_eq_eq, forall₂_iff, forall₂_iff_get, forall₂_iff_zip, forall₂_map_left_iff, forall₂_map_right_iff, forall₂_nil_left_iff, forall₂_nil_right_iff, forall₂_of_length_eq_of_get, forall₂_refl, forall₂_reverse_iff, forall₂_same, forall₂_take, forall₂_take_append, forall₂_zip, left_unique_forall₂', rel_append, rel_filter, rel_filterMap, rel_flatMap, rel_flatten, rel_foldl, rel_foldr, rel_map, rel_mem, rel_reverse, right_unique_forall₂', sublistForall₂_iff, sublistForall₂_map_left_iff, sublistForall₂_map_right_iff, tail_sublistForall₂_self, forall₂, forall₂, forall₂	47
Total	48

List

Definitions

Name	Category	Theorems
SublistForall₂ 📖	CompData	8 math math: SublistForall₂.is_refl, SublistForall₂.is_trans, tail_sublistForall₂_self, Set.PartiallyWellOrderedOn.partiallyWellOrderedOn_sublistForall₂, sublistForall₂_map_right_iff, Sublist.sublistForall₂, sublistForall₂_iff, sublistForall₂_map_left_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forall₂_and_left 📖	—	—	—	—	—
forall₂_cons_left_iff 📖	—	—	—	—	—
forall₂_cons_right_iff 📖	—	—	—	—	—
forall₂_drop 📖	—	—	—	—	—
forall₂_drop_append 📖	—	—	—	—	forall₂_drop
forall₂_eq_eq_eq 📖	—	—	—	—	forall₂_refl IsPreorder.toRefl IsEquiv.toIsPreorder eq_isEquiv
forall₂_iff 📖	—	—	—	—	—
forall₂_iff_get 📖	—	—	—	—	Forall₂.length_eq Forall₂.get forall₂_of_length_eq_of_get
forall₂_iff_zip 📖	—	—	—	—	Forall₂.length_eq forall₂_zip
forall₂_map_left_iff 📖	—	—	—	—	—
forall₂_map_right_iff 📖	—	—	—	—	—
forall₂_nil_left_iff 📖	—	—	—	—	—
forall₂_nil_right_iff 📖	—	—	—	—	—
forall₂_of_length_eq_of_get 📖	—	—	—	—	—
forall₂_refl 📖	—	—	—	—	forall₂_same refl
forall₂_reverse_iff 📖	—	—	—	—	rel_reverse
forall₂_same 📖	—	—	—	—	instIsEmptyFalse
forall₂_take 📖	—	—	—	—	—
forall₂_take_append 📖	—	—	—	—	forall₂_take
forall₂_zip 📖	—	—	—	—	—
left_unique_forall₂' 📖	—	Relator.LeftUnique	—	—	—
rel_append 📖	mathematical	—	Relator.LiftFun	—	—
rel_filter 📖	—	Relator.LiftFun	—	—	—
rel_filterMap 📖	mathematical	—	Relator.LiftFun	—	—
rel_flatMap 📖	mathematical	—	Relator.LiftFun Function.swap	—	rel_flatten rel_map
rel_flatten 📖	mathematical	—	Relator.LiftFun	—	rel_append
rel_foldl 📖	mathematical	—	Relator.LiftFun	—	—
rel_foldr 📖	mathematical	—	Relator.LiftFun	—	—
rel_map 📖	mathematical	—	Relator.LiftFun	—	—
rel_mem 📖	mathematical	Relator.BiUnique	Relator.LiftFun	—	Relator.rel_or Relator.rel_eq
rel_reverse 📖	mathematical	—	Relator.LiftFun	—	rel_append
right_unique_forall₂' 📖	—	Relator.RightUnique	—	—	—
sublistForall₂_iff 📖	mathematical	—	SublistForall₂	—	Sublist.cons_cons forall₂_nil_right_iff
sublistForall₂_map_left_iff 📖	mathematical	—	SublistForall₂	—	—
sublistForall₂_map_right_iff 📖	mathematical	—	SublistForall₂	—	—
tail_sublistForall₂_self 📖	mathematical	—	SublistForall₂	—	Sublist.sublistForall₂

List.Forall₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
flip 📖	—	—	—	—	—
get 📖	—	—	—	—	—
imp 📖	—	—	—	—	—
length_eq 📖	—	—	—	—	—
mp 📖	—	—	—	—	—

List.Sublist

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sublistForall₂ 📖	mathematical	—	List.SublistForall₂	—	List.sublistForall₂_iff List.forall₂_refl

List.SublistForall₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
is_refl 📖	mathematical	—	List.SublistForall₂	—	List.sublistForall₂_iff List.forall₂_refl
is_trans 📖	mathematical	—	IsTrans List.SublistForall₂	—	trans

Relator.BiUnique

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forall₂ 📖	—	Relator.BiUnique	—	—	Relator.LeftUnique.forall₂ Relator.RightUnique.forall₂

Relator.LeftUnique

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forall₂ 📖	—	Relator.LeftUnique	—	—	List.left_unique_forall₂'

Relator.RightUnique

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forall₂ 📖	—	Relator.RightUnique	—	—	List.right_unique_forall₂'

---

← Back to Index