Commit 2023-01-10 16:14 6ef0ef18

View on Github →

feat: port Data.List.Lattice (#1449)

feat: port Mathlib.Data.List.Lattice
Initial file copy from mathport
Mathbin -> Mathlib; add import to Mathlib.lean

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/List/Lattice.lean

added theorem List.Disjoint.symm

added theorem List.bagInter_nil

added theorem List.bagInter_nil_iff_inter_nil

added theorem List.bagInter_sublist_left

added theorem List.cons_bagInter_of_neg

added theorem List.cons_bagInter_of_pos

added theorem List.count_bagInter

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_bagInter

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_bagInter

added theorem List.sublist_suffix_of_union

added theorem List.subset_inter

added theorem List.suffix_union_right

added theorem List.union_sublist_append