Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-27 12:05 5292cf1f

View on Github →

Merge branch 'master' of https://github.com/leanprover/mathlib

Estimated changes

added def finset.card
added theorem finset.card_empty
added theorem finset.card_insert_le
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 def finset.erase
added theorem finset.erase_empty
added theorem finset.erase_insert
added theorem finset.erase_subset
added theorem finset.ext
added theorem finset.insert.comm
added def finset.insert
added theorem finset.insert_eq
added theorem finset.insert_erase
added theorem finset.insert_union
added def finset.inter
added theorem finset.inter_assoc
added theorem finset.inter_comm
added theorem finset.inter_empty
added theorem finset.inter_left_comm
added theorem finset.inter_self
added theorem finset.lt_of_mem_upto
added def finset.mem
added theorem finset.mem_empty_iff
added theorem finset.mem_erase_iff
added theorem finset.mem_insert
added theorem finset.mem_insert_iff
added theorem finset.mem_inter
added theorem finset.mem_inter_iff
added theorem finset.mem_list_of_mem
added theorem finset.mem_of_mem_list
added theorem finset.mem_singleton
added theorem finset.mem_to_finset
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_iff
added theorem finset.mem_upto_of_lt
added theorem finset.ne_of_mem_erase
added theorem finset.not_mem_empty
added theorem finset.not_mem_erase
added theorem finset.subset.antisymm
added theorem finset.subset.refl
added theorem finset.subset.trans
added def finset.subset
added theorem finset.subset_insert
added def finset.to_finset
added def finset.union
added theorem finset.union_assoc
added theorem finset.union_comm
added theorem finset.union_empty
added theorem finset.union_left_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