Commit 2023-01-06 11:42 da1884cd

View on Github →

feat: port Data.List.Forall2 (#1359)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/List/Forall2.lean

added theorem List.Forall₂.flip

added theorem List.Forall₂.imp

added theorem List.Forall₂.length_eq

added theorem List.Forall₂.mp

added theorem List.Forall₂.nthLe

added theorem List.Sublist.sublistForall₂

added inductive List.SublistForall₂

added theorem List.forall₂_and_left

added theorem List.forall₂_cons

added theorem List.forall₂_cons_left_iff

added theorem List.forall₂_cons_right_iff

added theorem List.forall₂_drop

added theorem List.forall₂_drop_append

added theorem List.forall₂_eq_eq_eq

added theorem List.forall₂_iff_nthLe

added theorem List.forall₂_iff_zip

added theorem List.forall₂_map_left_iff

added theorem List.forall₂_map_right_iff

added theorem List.forall₂_nil_left_iff

added theorem List.forall₂_nil_right_iff

added theorem List.forall₂_of_length_eq_of_nthLe

added theorem List.forall₂_refl

added theorem List.forall₂_reverse_iff

added theorem List.forall₂_same

added theorem List.forall₂_take

added theorem List.forall₂_take_append

added theorem List.forall₂_zip

added theorem List.left_unique_forall₂'

added theorem List.rel_append

added theorem List.rel_bind

added theorem List.rel_filter

added theorem List.rel_filterMap

added theorem List.rel_foldl

added theorem List.rel_foldr

added theorem List.rel_join

added theorem List.rel_map

added theorem List.rel_mem

added theorem List.rel_prod

added theorem List.rel_reverse

added theorem List.right_unique_forall₂'

added theorem List.sublistForall₂_iff

added theorem List.tail_sublistForall₂_self

added theorem Relator.BiUnique.forall₂

added theorem Relator.LeftUnique.forall₂

added theorem Relator.RightUnique.forall₂