Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-24 00:15 96e81faa

View on Github →

feat(data/(lazy_)list): various lemmas and definitions (#4172)

Estimated changes

added def lazy_list.attach
added theorem lazy_list.mem_cons
added theorem lazy_list.mem_nil
added def lazy_list.pmap
added theorem list.inter_reverse
added theorem list.mem_map_swap
added theorem list.mem_of_mem_drop
added theorem list.nth_eq_none_iff
added theorem list.nth_injective
added theorem list.reverse_take
added theorem list.sizeof_slice_lt
added theorem list.slice_eq
added def list.slice
added theorem list.perm.drop_inter
added theorem list.perm.inter_append
added theorem list.perm.slice_inter
added theorem list.perm.take_inter
added theorem list.sizeof_kerase
added theorem list.nth_zip_eq_some
added theorem list.nth_zip_with
added theorem prod.fst_to_sigma
added theorem prod.snd_to_sigma
added def prod.to_sigma