Commit 2023-01-16 16:20 4c08b36f

View on Github →

feat: port Data.Finset.Card (#1589)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finset/Card.lean

added def Finset.card

added theorem Finset.card_attach

added theorem Finset.card_congr

added theorem Finset.card_cons

added theorem Finset.card_def

added theorem Finset.card_disjUnion

added theorem Finset.card_disjoint_union

added theorem Finset.card_doubleton

added theorem Finset.card_empty

added theorem Finset.card_eq_of_bijective

added theorem Finset.card_eq_one

added theorem Finset.card_eq_succ

added theorem Finset.card_eq_three

added theorem Finset.card_eq_two

added theorem Finset.card_eq_zero

added theorem Finset.card_erase_add_one

added theorem Finset.card_erase_eq_ite

added theorem Finset.card_erase_le

added theorem Finset.card_erase_lt_of_mem

added theorem Finset.card_erase_of_mem

added theorem Finset.card_filter_le

added theorem Finset.card_image_iff

added theorem Finset.card_image_le

added theorem Finset.card_image_of_injOn

added theorem Finset.card_image_of_injective

added theorem Finset.card_insert_eq_ite

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_inter_add_card_union

added theorem Finset.card_le_card_of_inj_on

added theorem Finset.card_le_card_sdiff_add_card

added theorem Finset.card_le_of_subset

added theorem Finset.card_le_one

added theorem Finset.card_le_one_iff

added theorem Finset.card_le_one_iff_subset_singleton

added theorem Finset.card_le_one_of_subsingleton

added theorem Finset.card_lt_card

added theorem Finset.card_map

added theorem Finset.card_mk

added theorem Finset.card_mono

added theorem Finset.card_ne_zero_of_mem

added theorem Finset.card_pos

added theorem Finset.card_range

added theorem Finset.card_sdiff

added theorem Finset.card_sdiff_add_card

added theorem Finset.card_sdiff_add_card_eq_card

added theorem Finset.card_singleton

added theorem Finset.card_singleton_inter

added theorem Finset.card_subtype

added theorem Finset.card_union_add_card_inter

added theorem Finset.card_union_eq

added theorem Finset.card_union_le

added theorem Finset.case_strong_induction_on

added theorem Finset.eq_of_subset_of_card_le

added theorem Finset.eq_of_superset_of_card_ge

added theorem Finset.exists_eq_insert_iff

added theorem Finset.exists_intermediate_set

added theorem Finset.exists_ne_map_eq_of_card_lt_of_maps_to

added theorem Finset.exists_ne_of_one_lt_card

added theorem Finset.exists_smaller_set

added theorem Finset.exists_subset_or_subset_of_two_mul_lt_card

added theorem Finset.fiber_card_ne_zero_iff_mem_image

added theorem Finset.filter_card_add_filter_neg_card_eq_card

added theorem Finset.filter_card_eq

added theorem Finset.injOn_of_card_image_eq

added theorem Finset.inj_on_of_surj_on_of_card_le

added theorem Finset.le_card_of_inj_on_range

added theorem Finset.le_card_sdiff

added theorem Finset.length_toList

added theorem Finset.lt_wf

added theorem Finset.map_eq_of_subset

added theorem Finset.one_lt_card

added theorem Finset.one_lt_card_iff

added theorem Finset.pred_card_le_card_erase

added def Finset.strongDownwardInduction

added def Finset.strongDownwardInductionOn

added theorem Finset.strongDownwardInductionOn_eq

added theorem Finset.strongDownwardInduction_eq

added def Finset.strongInduction

added def Finset.strongInductionOn

added theorem Finset.strongInductionOn_eq

added theorem Finset.strongInduction_eq

added theorem Finset.subset_iff_eq_of_card_le

added theorem Finset.surj_on_of_inj_on_of_card_le

added theorem Finset.two_lt_card

added theorem Finset.two_lt_card_iff

added theorem List.card_toFinset

added theorem List.toFinset_card_le

added theorem List.toFinset_card_of_nodup

added theorem Multiset.card_toFinset

added theorem Multiset.toFinset_card_le

added theorem Multiset.toFinset_card_of_nodup