Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-03-13 05:57 4ceb545f

View on Github →

feat(data/list/basic): stuff about list.sublists

Estimated changes

Modified analysis/topology/topological_space.lean

Modified data/list/basic.lean

added theorem list.bind_eq_bind

added theorem list.bind_ret_eq_map

added theorem list.cons_subset

modified theorem list.cons_subset_of_subset_of_mem

added theorem list.length_eq_zero

added theorem list.length_sublists

added theorem list.lex.imp

added inductive list.lex

added theorem list.lex_append_left

added theorem list.lex_append_right

added theorem list.lex_ne_iff

added theorem list.map_eq_map

added theorem list.map_ret_sublist_sublists

modified theorem list.mem_sublists

added theorem list.ne_of_lex_ne

added theorem list.nodup_sublists

added theorem list.pairwise_sublists

added theorem list.reverse_eq_nil

added theorem list.reverse_inj

modified theorem list.reverse_nil

added theorem list.reverse_rec_on

modified theorem list.reverse_singleton

added theorem list.sublists_append

added theorem list.sublists_aux_cons_append

added theorem list.sublists_aux_cons_eq_sublists_aux₁

deleted theorem list.sublists_aux_eq_foldl

added theorem list.sublists_aux_eq_foldr.aux

added theorem list.sublists_aux_eq_foldr

added theorem list.sublists_aux_ne_nil

added def list.sublists_aux₁

added theorem list.sublists_aux₁_append

added theorem list.sublists_aux₁_bind

added theorem list.sublists_aux₁_concat

added theorem list.sublists_aux₁_eq_sublists_aux

added theorem list.sublists_concat

added theorem list.sublists_nil

added theorem list.sublists_singleton

added theorem list.subset_def