Sublists

📁 Source: Mathlib/Data/List/Sublists.lean

Statistics

Metric	Count
Definitions `sublists'Aux`, `sublistsAux`, `sublistsLen`, `sublistsLenAux`	4
Theorems `of_sublists`, `of_sublists'`, `sublists`, `sublists'`, `length_of_sublistsLen`, `length_sublists`, `length_sublists'`, `length_sublistsLen`, `map_pure_sublist_sublists`, `mem_sublists`, `mem_sublists'`, `mem_sublistsLen`, `mem_sublistsLen_self`, `nodup_sublists`, `nodup_sublists'`, `nodup_sublistsLen`, `pairwise_sublists`, `range_bind_sublistsLen_perm`, `revzip_sublists`, `revzip_sublists'`, `sublists'Aux_eq_array_foldl`, `sublists'Aux_eq_map`, `sublists'_cons`, `sublists'_eq_sublists`, `sublists'_eq_sublists'Aux`, `sublists'_map`, `sublists'_nil`, `sublists'_reverse`, `sublists'_singleton`, `sublistsAux_eq_array_foldl`, `sublistsAux_eq_flatMap`, `sublistsLenAux_append`, `sublistsLenAux_eq`, `sublistsLenAux_zero`, `sublistsLen_length`, `sublistsLen_of_length_lt`, `sublistsLen_one`, `sublistsLen_sublist_of_sublist`, `sublistsLen_sublist_sublists'`, `sublistsLen_succ_cons`, `sublistsLen_succ_nil`, `sublistsLen_zero`, `sublists_append`, `sublists_concat`, `sublists_cons`, `sublists_cons_perm_append`, `sublists_eq_sublists'`, `sublists_map`, `sublists_nil`, `sublists_perm_sublists'`, `sublists_reverse`, `sublists_singleton`	52
Total	56

List

Definitions

Name	Category	Theorems
`sublists'Aux` 📖	CompOp	3 math math: `sublists'Aux_eq_map`, `sublists'_eq_sublists'Aux`, `sublists'Aux_eq_array_foldl`
`sublistsAux` 📖	CompOp	2 math math: `sublistsAux_eq_array_foldl`, `sublistsAux_eq_flatMap`
`sublistsLen` 📖	CompOp	16 math math: `Multiset.powersetCardAux_eq_map_coe`, `sublistsLen_length`, `sublistsLenAux_eq`, `sublistsLen_one`, `nodup_sublistsLen`, `Multiset.powersetCard_coe`, `range_bind_sublistsLen_perm`, `mem_sublistsLen`, `length_sublistsLen`, `sublistsLen_succ_cons`, `mem_sublistsLen_self`, `sublistsLen_of_length_lt`, `sublistsLen_sublist_of_sublist`, `sublistsLen_sublist_sublists'`, `sublistsLen_succ_nil`, `sublistsLen_zero`
`sublistsLenAux` 📖	CompOp	3 math math: `sublistsLenAux_zero`, `sublistsLenAux_eq`, `sublistsLenAux_append`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`length_of_sublistsLen` 📖	—	`sublistsLen`	—	—	`sublistsLen_zero` `sublistsLen_succ_cons`
`length_sublists` 📖	—	—	—	—	`sublists_eq_sublists'` `length_sublists'`
`length_sublists'` 📖	—	—	—	—	`sublists'_cons`
`length_sublistsLen` 📖	mathematical	—	`sublistsLen` `Nat.choose`	—	`sublistsLen_zero` `Nat.choose_zero_right` `sublistsLen_succ_cons` `Nat.choose_succ_succ`
`map_pure_sublist_sublists` 📖	mathematical	—	`instAlternativeMonad_mathlib`	—	`sublists_concat` `mem_sublists`
`mem_sublists` 📖	—	—	—	—	`mem_sublists'` `sublists'_reverse` `mem_map_of_injective` `reverse_injective`
`mem_sublists'` 📖	—	—	—	—	`sublists'_cons` `sublist_cons_of_sublist` `Sublist.cons_cons`
`mem_sublistsLen` 📖	mathematical	—	`sublistsLen`	—	`mem_sublists'` `sublistsLen_sublist_sublists'` `length_of_sublistsLen` `mem_sublistsLen_self`
`mem_sublistsLen_self` 📖	mathematical	—	`sublistsLen`	—	`sublistsLen_zero` `sublistsLen_succ_cons`
`nodup_sublists` 📖	—	—	—	—	`Nodup.of_map` `map_pure_sublist_sublists` `Lex.to_ne` `pairwise_sublists`
`nodup_sublists'` 📖	—	—	—	—	`sublists'_eq_sublists` `nodup_map_iff` `reverse_injective` `nodup_sublists` `nodup_reverse`
`nodup_sublistsLen` 📖	mathematical	—	`sublistsLen`	—	`Lex.to_ne` `Pairwise.sublists'` `sublistsLen_sublist_sublists'`
`pairwise_sublists` 📖	mathematical	—	`Function.onFun`	—	`Pairwise.sublists'` `sublists'_reverse`
`range_bind_sublistsLen_perm` 📖	mathematical	—	`sublistsLen`	—	`sublistsLen_zero` `sublistsLen_succ_cons` `sublists'_cons` `flatMap_append_perm` `sublistsLen_of_length_lt`
`revzip_sublists` 📖	—	—	—	—	`length_sublists` `sublists_concat` `revzip.eq_1`
`revzip_sublists'` 📖	—	—	—	—	`length_sublists'` `sublists'_cons` `revzip.eq_1`
`sublists'Aux_eq_array_foldl` 📖	mathematical	—	`sublists'Aux`	—	`sublists'Aux.eq_1`
`sublists'Aux_eq_map` 📖	mathematical	—	`sublists'Aux`	—	`sublists'Aux.eq_1`
`sublists'_cons` 📖	—	—	—	—	`sublists'_eq_sublists'Aux` `sublists'Aux_eq_map`
`sublists'_eq_sublists` 📖	—	—	—	—	`sublists'_reverse`
`sublists'_eq_sublists'Aux` 📖	mathematical	—	`sublists'Aux`	—	`sublists'Aux_eq_array_foldl`
`sublists'_map` 📖	—	—	—	—	`sublists'_cons`
`sublists'_nil` 📖	—	—	—	—	—
`sublists'_reverse` 📖	—	—	—	—	`sublists_eq_sublists'`
`sublists'_singleton` 📖	—	—	—	—	—
`sublistsAux_eq_array_foldl` 📖	mathematical	—	`sublistsAux`	—	—
`sublistsAux_eq_flatMap` 📖	mathematical	—	`sublistsAux`	—	`sublistsAux.eq_1`
`sublistsLenAux_append` 📖	mathematical	—	`sublistsLenAux`	—	`sublistsLenAux.eq_def`
`sublistsLenAux_eq` 📖	mathematical	—	`sublistsLenAux` `sublistsLen`	—	`sublistsLen.eq_1` `sublistsLenAux_append`
`sublistsLenAux_zero` 📖	mathematical	—	`sublistsLenAux`	—	—
`sublistsLen_length` 📖	mathematical	—	`sublistsLen`	—	`sublistsLen_succ_cons` `sublistsLen_of_length_lt`
`sublistsLen_of_length_lt` 📖	mathematical	—	`sublistsLen`	—	`Iff.not` `mem_sublistsLen` `LT.lt.not_ge` `LT.lt.trans_eq`
`sublistsLen_one` 📖	mathematical	—	`sublistsLen`	—	`sublistsLen_succ_nil` `sublistsLen_succ_cons` `sublistsLen_zero`
`sublistsLen_sublist_of_sublist` 📖	mathematical	—	`sublistsLen`	—	`sublistsLen_zero` `sublistsLen_succ_cons`
`sublistsLen_sublist_sublists'` 📖	mathematical	—	`sublistsLen`	—	`sublistsLen_zero` `sublistsLen_succ_cons` `sublists'_cons`
`sublistsLen_succ_cons` 📖	mathematical	—	`sublistsLen`	—	`sublistsLen.eq_1` `sublistsLenAux.eq_3` `sublistsLenAux_eq`
`sublistsLen_succ_nil` 📖	mathematical	—	`sublistsLen`	—	—
`sublistsLen_zero` 📖	mathematical	—	`sublistsLen`	—	`sublistsLenAux_zero`
`sublists_append` 📖	mathematical	—	`instMonad`	—	—
`sublists_concat` 📖	—	—	—	—	`sublists_append` `sublists_singleton` `bind_eq_flatMap`
`sublists_cons` 📖	mathematical	—	`instMonad`	—	`sublists_append`
`sublists_cons_perm_append` 📖	—	—	—	—	`sublists_perm_sublists'` `sublists'_cons`
`sublists_eq_sublists'` 📖	—	—	—	—	`sublists_reverse`
`sublists_map` 📖	—	—	—	—	`sublists_cons` `bind_eq_flatMap`
`sublists_nil` 📖	—	—	—	—	—
`sublists_perm_sublists'` 📖	—	—	—	—	`sublists_map` `sublists'_map` `nodup_sublists` `nodup_sublists'`
`sublists_reverse` 📖	—	—	—	—	`sublists_append` `sublists'_cons`
`sublists_singleton` 📖	—	—	—	—	—

List.Nodup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_sublists` 📖	—	—	—	—	`List.nodup_sublists`
`of_sublists'` 📖	—	—	—	—	`List.nodup_sublists'`
`sublists` 📖	—	—	—	—	`List.nodup_sublists`

List.Pairwise

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sublists'` 📖	mathematical	—	`Function.swap`	—	`List.sublists'_cons`

---

← Back to Index