Commit 2022-09-26 05:32 a48b8eff

View on Github →

feat(data/list/basic): list.head, list.head', and list.tail are surjective (#16625) Also add list.eq_cons_of_mem_head', a more specific version of list.mem_of_mem_head'

Estimated changes

Modified src/data/list/basic.lean

added theorem list.eq_cons_of_mem_head'

modified theorem list.mem_of_mem_head'

added theorem list.surjective_head'

added theorem list.surjective_head

added theorem list.surjective_tail