Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-24 13:34 696f07f2

View on Github →

split(data/list/lattice): split off data.list.basic (#9906)

Estimated changes

Deleted src/data/list/bag_inter.lean

deleted theorem list.bag_inter_nil

deleted theorem list.bag_inter_nil_iff_inter_nil

deleted theorem list.bag_inter_sublist_left

deleted theorem list.cons_bag_inter_of_neg

deleted theorem list.cons_bag_inter_of_pos

deleted theorem list.count_bag_inter

deleted theorem list.mem_bag_inter

deleted theorem list.nil_bag_inter

Modified src/data/list/basic.lean

deleted theorem list.cons_union

deleted theorem list.disjoint.symm

deleted theorem list.disjoint_append_left

deleted theorem list.disjoint_append_right

deleted theorem list.disjoint_comm

deleted theorem list.disjoint_cons_left

deleted theorem list.disjoint_cons_right

deleted theorem list.disjoint_iff_ne

deleted theorem list.disjoint_left

deleted theorem list.disjoint_nil_left

deleted theorem list.disjoint_nil_right

deleted theorem list.disjoint_of_disjoint_append_left_left

deleted theorem list.disjoint_of_disjoint_append_left_right

deleted theorem list.disjoint_of_disjoint_append_right_left

deleted theorem list.disjoint_of_disjoint_append_right_right

deleted theorem list.disjoint_of_disjoint_cons_left

deleted theorem list.disjoint_of_disjoint_cons_right

deleted theorem list.disjoint_of_subset_left

deleted theorem list.disjoint_of_subset_right

deleted theorem list.disjoint_right

deleted theorem list.disjoint_singleton

deleted theorem list.disjoint_take_drop

deleted theorem list.forall_mem_inter_of_forall_left

deleted theorem list.forall_mem_inter_of_forall_right

deleted theorem list.forall_mem_of_forall_mem_union_left

deleted theorem list.forall_mem_of_forall_mem_union_right

deleted theorem list.forall_mem_union

deleted theorem list.inter_cons_of_mem

deleted theorem list.inter_cons_of_not_mem

deleted theorem list.inter_eq_nil_iff_disjoint

deleted theorem list.inter_nil

deleted theorem list.inter_reverse

deleted theorem list.inter_subset_left

deleted theorem list.inter_subset_right

deleted theorem list.mem_inter

deleted theorem list.mem_inter_of_mem_of_mem

deleted theorem list.mem_of_mem_inter_left

deleted theorem list.mem_of_mem_inter_right

deleted theorem list.mem_union

deleted theorem list.mem_union_left

deleted theorem list.mem_union_right

deleted theorem list.nil_union

deleted theorem list.singleton_disjoint

deleted theorem list.sublist_suffix_of_union

deleted theorem list.subset_inter

deleted theorem list.suffix_union_right

deleted theorem list.union_sublist_append

Modified src/data/list/default.lean

Modified src/data/list/intervals.lean

Created src/data/list/lattice.lean

added theorem list.bag_inter_nil

added theorem list.bag_inter_nil_iff_inter_nil

added theorem list.bag_inter_sublist_left

added theorem list.cons_bag_inter_of_neg

added theorem list.cons_bag_inter_of_pos

added theorem list.cons_union

added theorem list.count_bag_inter

added theorem list.disjoint.symm

added theorem list.disjoint_append_left

added theorem list.disjoint_append_right

added theorem list.disjoint_comm

added theorem list.disjoint_cons_left

added theorem list.disjoint_cons_right

added theorem list.disjoint_iff_ne

added theorem list.disjoint_left

added theorem list.disjoint_nil_left

added theorem list.disjoint_nil_right

added theorem list.disjoint_of_disjoint_append_left_left

added theorem list.disjoint_of_disjoint_append_left_right

added theorem list.disjoint_of_disjoint_append_right_left

added theorem list.disjoint_of_disjoint_append_right_right

added theorem list.disjoint_of_disjoint_cons_left

added theorem list.disjoint_of_disjoint_cons_right

added theorem list.disjoint_of_subset_left

added theorem list.disjoint_of_subset_right

added theorem list.disjoint_right

added theorem list.disjoint_singleton

added theorem list.disjoint_take_drop

added theorem list.forall_mem_inter_of_forall_left

added theorem list.forall_mem_inter_of_forall_right

added theorem list.forall_mem_of_forall_mem_union_left

added theorem list.forall_mem_of_forall_mem_union_right

added theorem list.forall_mem_union

added theorem list.inter_cons_of_mem

added theorem list.inter_cons_of_not_mem

added theorem list.inter_eq_nil_iff_disjoint

added theorem list.inter_nil

added theorem list.inter_reverse

added theorem list.inter_subset_left

added theorem list.inter_subset_right

added theorem list.mem_bag_inter

added theorem list.mem_inter

added theorem list.mem_inter_of_mem_of_mem

added theorem list.mem_of_mem_inter_left

added theorem list.mem_of_mem_inter_right

added theorem list.mem_union

added theorem list.mem_union_left

added theorem list.mem_union_right

added theorem list.nil_bag_inter

added theorem list.nil_union

added theorem list.singleton_disjoint

added theorem list.sublist_suffix_of_union

added theorem list.subset_inter

added theorem list.suffix_union_right

added theorem list.union_sublist_append

Modified src/data/list/nodup.lean

Modified src/data/list/perm.lean