Commit 2024-10-17 15:41 0456b9a1

View on Github →

feat: #s as notation for Finset.card s (#17646) I believe it is time that we finally introduce this notation. This makes serious finset calculations significantly nicer (see eg #5297) and is standard notation. |s| would be an alternative, but absolute value elaboration is very complicated like that, so I would rather not, and #{x | p x} looks nicer than |{x | p x}| (although in return |s ∩ t| looks nicer than #(s ∩ t)). I am scoping the notation to the Finset namespace to avoid clashes with Cardinal.mk, which also uses that notation.

Estimated changes

Modified Mathlib/Data/Finset/Card.lean

modified theorem Finset.card_attach

modified theorem Finset.card_cons

modified theorem Finset.card_def

modified theorem Finset.card_disjUnion

modified theorem Finset.card_empty

modified theorem Finset.card_eq_one

modified theorem Finset.card_eq_succ

modified theorem Finset.card_eq_three

modified theorem Finset.card_eq_two

modified theorem Finset.card_eq_zero

modified theorem Finset.card_equiv

modified theorem Finset.card_erase_add_one

modified theorem Finset.card_erase_eq_ite

modified theorem Finset.card_erase_le

modified theorem Finset.card_erase_lt_of_mem

modified theorem Finset.card_erase_of_mem

modified theorem Finset.card_image_iff

modified theorem Finset.card_image_le

modified theorem Finset.card_image_of_injOn

modified theorem Finset.card_insert_eq_ite

modified theorem Finset.card_insert_le

modified theorem Finset.card_insert_of_mem

modified theorem Finset.card_insert_of_not_mem

modified theorem Finset.card_inter

modified theorem Finset.card_le_card

modified theorem Finset.card_le_card_of_surjOn

modified theorem Finset.card_le_card_sdiff_add_card

modified theorem Finset.card_le_five

modified theorem Finset.card_le_four

modified theorem Finset.card_le_one

modified theorem Finset.card_le_one_iff

modified theorem Finset.card_le_one_iff_subset_singleton

modified theorem Finset.card_le_one_iff_subsingleton_coe

modified theorem Finset.card_le_one_of_subsingleton

modified theorem Finset.card_le_six

modified theorem Finset.card_le_three

modified theorem Finset.card_le_two

modified theorem Finset.card_map

modified theorem Finset.card_mk

modified theorem Finset.card_ne_zero

modified theorem Finset.card_ne_zero_of_mem

modified theorem Finset.card_pair

modified theorem Finset.card_pair_eq_one_or_two

modified theorem Finset.card_pos

modified theorem Finset.card_range

modified theorem Finset.card_sdiff

modified theorem Finset.card_sdiff_add_card

modified theorem Finset.card_sdiff_add_card_eq_card

modified theorem Finset.card_sdiff_comm

modified theorem Finset.card_singleton

modified theorem Finset.card_singleton_inter

modified theorem Finset.card_union

modified theorem Finset.card_union_eq_card_add_card

modified theorem Finset.card_union_le

modified theorem Finset.card_val

modified theorem Finset.cast_card_sdiff

modified theorem Finset.eq_of_subset_of_card_le

modified theorem Finset.eq_of_superset_of_card_ge

modified theorem Finset.exists_intermediate_set

modified theorem Finset.exists_mem_ne

modified theorem Finset.exists_ne_map_eq_of_card_lt_of_maps_to

modified theorem Finset.exists_ne_of_one_lt_card

modified theorem Finset.exists_smaller_set

modified theorem Finset.exists_subset_card_eq

modified theorem Finset.exists_subsuperset_card_eq

modified theorem Finset.filter_card_eq

modified theorem Finset.injOn_of_card_image_eq

modified theorem Finset.le_card_iff_exists_subset_card

modified theorem Finset.le_card_sdiff

modified theorem Finset.length_toList

modified theorem Finset.one_le_card

modified theorem Finset.one_lt_card

modified theorem Finset.one_lt_card_iff

modified theorem Finset.one_lt_card_iff_nontrivial

modified theorem Finset.pred_card_le_card_erase

modified theorem Finset.subset_iff_eq_of_card_le

modified theorem Finset.two_lt_card

modified theorem Finset.two_lt_card_iff

modified theorem List.card_toFinset

modified theorem List.toFinset_card_le

modified theorem List.toFinset_card_of_nodup

modified theorem Multiset.card_toFinset

modified theorem Multiset.toFinset_card_le