Commit 2023-01-13 10:47 fb6c6c41

View on Github →

feat: port Data.List.Sublists (#1494)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/List/Defs.lean

deleted def List.sublistsAux₁

Modified Mathlib/Data/List/Range.lean

added theorem List.finRange_map_get

Created Mathlib/Data/List/Sublists.lean

added theorem List.Pairwise.sublists'

added theorem List.length_of_sublistsLen

added theorem List.length_sublists'

added theorem List.length_sublists

added theorem List.length_sublistsLen

added theorem List.map_ret_sublist_sublists

added theorem List.mem_sublists'

added theorem List.mem_sublists

added theorem List.mem_sublistsLen

added theorem List.mem_sublistsLen_self

added theorem List.nodup_sublists'

added theorem List.nodup_sublists

added theorem List.nodup_sublistsLen

added theorem List.pairwise_sublists

added theorem List.range_bind_sublistsLen_perm

added theorem List.revzip_sublists'

added theorem List.revzip_sublists

added def List.sublists'Aux

added theorem List.sublists'Aux_eq_array_foldl

added theorem List.sublists'Aux_eq_map

added theorem List.sublists'_cons

added theorem List.sublists'_eq_sublists'Aux

added theorem List.sublists'_eq_sublists

added theorem List.sublists'_map

added theorem List.sublists'_nil

added theorem List.sublists'_reverse

added theorem List.sublists'_singleton

added def List.sublistsAux

added theorem List.sublistsAux_eq_array_foldl

added theorem List.sublistsAux_eq_bind

added def List.sublistsLen

added def List.sublistsLenAux

added theorem List.sublistsLenAux_append

added theorem List.sublistsLenAux_eq

added theorem List.sublistsLenAux_zero

added theorem List.sublistsLen_length

added theorem List.sublistsLen_of_length_lt

added theorem List.sublistsLen_sublist_of_sublist

added theorem List.sublistsLen_sublist_sublists'

added theorem List.sublistsLen_succ_cons

added theorem List.sublistsLen_succ_nil

added theorem List.sublistsLen_zero

added theorem List.sublists_append

added theorem List.sublists_concat

added theorem List.sublists_cons

added theorem List.sublists_cons_perm_append

added theorem List.sublists_eq_sublists'

added theorem List.sublists_eq_sublistsAux

added theorem List.sublists_map

added theorem List.sublists_nil

added theorem List.sublists_perm_sublists'

added theorem List.sublists_reverse

added theorem List.sublists_singleton