Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-24 16:21 7df585ef

View on Github →

feat(data/finset): add basics for finsets

Estimated changes

Created data/finset/basic.lean

added def finset.card

added theorem finset.card_empty

added theorem finset.card_erase_of_mem

added theorem finset.card_erase_of_not_mem

added theorem finset.card_insert_le

added theorem finset.card_insert_of_mem

added theorem finset.card_insert_of_not_mem

added theorem finset.card_upto

added def finset.empty

added theorem finset.empty_inter

added theorem finset.empty_subset

added theorem finset.empty_union

added theorem finset.eq_empty_of_card_eq_zero

added theorem finset.eq_empty_of_forall_not_mem

added theorem finset.eq_empty_of_subset_empty

added theorem finset.eq_of_mem_singleton

added theorem finset.eq_of_singleton_eq

added theorem finset.eq_of_subset_of_subset

added theorem finset.eq_or_mem_of_mem_insert

added def finset.erase

added theorem finset.erase_empty

added theorem finset.erase_eq_of_not_mem

added theorem finset.erase_insert

added theorem finset.erase_insert_subset

added theorem finset.erase_subset

added theorem finset.erase_subset_erase

added theorem finset.erase_subset_of_subset_insert

added theorem finset.exists_mem_empty_eq

added theorem finset.exists_mem_empty_iff

added theorem finset.exists_mem_insert_eq

added theorem finset.exists_mem_insert_iff

added theorem finset.exists_mem_of_ne_empty

added theorem finset.ext

added theorem finset.forall_mem_empty_eq

added theorem finset.forall_mem_empty_iff

added theorem finset.forall_mem_insert_eq

added theorem finset.forall_mem_insert_iff

added theorem finset.forall_of_forall_insert

added theorem finset.insert.comm

added def finset.insert

added theorem finset.insert_eq

added theorem finset.insert_eq_of_mem

added theorem finset.insert_erase

added theorem finset.insert_erase_subset

added theorem finset.insert_subset_insert

added theorem finset.insert_union

added def finset.inter

added theorem finset.inter_assoc

added theorem finset.inter_comm

added theorem finset.inter_distrib_left

added theorem finset.inter_distrib_right

added theorem finset.inter_empty

added theorem finset.inter_left_comm

added theorem finset.inter_right_comm

added theorem finset.inter_self

added theorem finset.lt_of_mem_upto

added def finset.mem

added theorem finset.mem_empty_eq

added theorem finset.mem_empty_iff

added theorem finset.mem_erase_eq

added theorem finset.mem_erase_iff

added theorem finset.mem_erase_of_ne_of_mem

added theorem finset.mem_insert

added theorem finset.mem_insert_eq

added theorem finset.mem_insert_iff

added theorem finset.mem_insert_of_mem

added theorem finset.mem_inter

added theorem finset.mem_inter_eq

added theorem finset.mem_inter_iff

added theorem finset.mem_list_of_mem

added theorem finset.mem_of_mem_erase

added theorem finset.mem_of_mem_insert_of_ne

added theorem finset.mem_of_mem_inter_left

added theorem finset.mem_of_mem_inter_right

added theorem finset.mem_of_mem_list

added theorem finset.mem_of_subset_of_mem

added theorem finset.mem_or_mem_of_mem_union

added theorem finset.mem_singleton

added theorem finset.mem_singleton_iff

added theorem finset.mem_singleton_of_eq

added theorem finset.mem_to_finset

added theorem finset.mem_to_finset_of_nodup

added theorem finset.mem_union_eq

added theorem finset.mem_union_iff

added theorem finset.mem_union_l

added theorem finset.mem_union_left

added theorem finset.mem_union_r

added theorem finset.mem_union_right

added theorem finset.mem_upto_eq

added theorem finset.mem_upto_iff

added theorem finset.mem_upto_of_lt

added theorem finset.mem_upto_succ_of_mem_upto

added theorem finset.ne_empty_of_card_eq_succ

added theorem finset.ne_of_mem_erase

added theorem finset.not_mem_empty

added theorem finset.not_mem_erase

added theorem finset.pair_eq_singleton

added theorem finset.perm_insert_cons_of_not_mem

added theorem finset.singleton_inter_of_mem

added theorem finset.singleton_inter_of_not_mem

added theorem finset.singleton_ne_empty

added theorem finset.subset.antisymm

added theorem finset.subset.refl

added theorem finset.subset.trans

added def finset.subset

added def finset.subset_aux

added theorem finset.subset_empty_iff

added theorem finset.subset_insert

added theorem finset.subset_insert_iff

added theorem finset.subset_insert_of_erase_subset

added theorem finset.subset_of_forall

added def finset.to_finset

added theorem finset.to_finset_eq_of_nodup

added def finset.to_finset_of_nodup

added def finset.union

added theorem finset.union_assoc

added theorem finset.union_comm

added theorem finset.union_distrib_left

added theorem finset.union_distrib_right

added theorem finset.union_empty

added theorem finset.union_left_comm

added theorem finset.union_right_comm

added theorem finset.union_self

added def finset.upto

added theorem finset.upto_succ

added theorem finset.upto_zero

added def finset

added def nodup_list

added def to_nodup_list

added def to_nodup_list_of_nodup

Modified data/list/set.lean

added theorem list.length_erase_of_not_mem