Commit 2021-04-24 22:17 77168704

View on Github →

feat(data/list/forall2): defines sublist_forall2 relation (#7165) Defines the sublist_forall₂ relation, indicating that one list is related by forall₂ to a sublist of another. Provides two lemmas, head_mem_self and mem_of_mem_tail, which will be useful when proving Higman's Lemma about the sublist_forall₂ relation.

Estimated changes

Modified src/data/list/basic.lean

added theorem list.head_mem_self

added theorem list.tail_sublist

modified theorem list.tail_subset

Modified src/data/list/forall2.lean

added theorem list.sublist.sublist_forall₂

added inductive list.sublist_forall₂

added theorem list.sublist_forall₂_iff

added theorem list.tail_sublist_forall₂_self