Commit 2023-06-06 18:52 e77b8f01

View on Github →

feat: port Data.Set.Ncard (#4591) A port of the newly added ncard file.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Set/Ncard.lean

added theorem Set.Finite_of_ncard_ne_zero

added theorem Set.Finite_of_ncard_pos

added theorem Set.Infinite.exists_subset_ncard_eq

added theorem Set.Infinite.exists_supset_ncard_eq

added theorem Set.Infinite.ncard

added theorem Set.Nat.card_coe_set_eq

added theorem Set.diff_nonempty_of_ncard_lt_ncard

added theorem Set.eq_insert_of_ncard_eq_succ

added theorem Set.eq_of_subset_of_ncard_le

added theorem Set.exists_eq_insert_iff_ncard

added theorem Set.exists_intermediate_Set'

added theorem Set.exists_intermediate_Set

added theorem Set.exists_mem_not_mem_of_ncard_lt_ncard

added theorem Set.exists_ne_map_eq_of_ncard_lt_of_maps_to

added theorem Set.exists_ne_of_one_lt_ncard

added theorem Set.exists_smaller_Set

added theorem Set.exists_subset_or_subset_of_two_mul_lt_ncard

added theorem Set.fiber_ncard_ne_zero_iff_mem_image

added theorem Set.injOn_of_ncard_image_eq

added theorem Set.inj_on_of_surj_on_of_ncard_le

added theorem Set.le_ncard_diff

added theorem Set.le_ncard_of_inj_on_range

added theorem Set.map_eq_of_subset

added theorem Set.ncard_add_ncard_compl

added theorem Set.ncard_coe_Finset

added theorem Set.ncard_congr

added theorem Set.ncard_def

added theorem Set.ncard_diff

added theorem Set.ncard_diff_add_ncard

added theorem Set.ncard_diff_add_ncard_eq_ncard

added theorem Set.ncard_diff_singleton_add_one

added theorem Set.ncard_diff_singleton_le

added theorem Set.ncard_diff_singleton_lt_of_mem

added theorem Set.ncard_diff_singleton_of_mem

added theorem Set.ncard_empty

added theorem Set.ncard_eq_ncard_iff_ncard_diff_eq_ncard_diff

added theorem Set.ncard_eq_ofBijective

added theorem Set.ncard_eq_one

added theorem Set.ncard_eq_succ

added theorem Set.ncard_eq_three

added theorem Set.ncard_eq_toFinset_card'

added theorem Set.ncard_eq_toFinset_card

added theorem Set.ncard_eq_two

added theorem Set.ncard_eq_zero

added theorem Set.ncard_exchange'

added theorem Set.ncard_exchange

added theorem Set.ncard_image_iff

added theorem Set.ncard_image_le

added theorem Set.ncard_image_ofInjective

added theorem Set.ncard_image_of_injOn

added theorem Set.ncard_insert_eq_ite

added theorem Set.ncard_insert_le

added theorem Set.ncard_insert_of_mem

added theorem Set.ncard_insert_of_not_mem

added theorem Set.ncard_inter_add_ncard_diff_eq_ncard

added theorem Set.ncard_inter_add_ncard_union

added theorem Set.ncard_inter_le_ncard_left

added theorem Set.ncard_inter_le_ncard_right

added theorem Set.ncard_le_ncard_diff_add_ncard

added theorem Set.ncard_le_ncard_iff_ncard_diff_le_ncard_diff

added theorem Set.ncard_le_ncard_insert

added theorem Set.ncard_le_ncard_of_injOn

added theorem Set.ncard_le_of_subset

added theorem Set.ncard_le_one

added theorem Set.ncard_le_one_iff

added theorem Set.ncard_le_one_iff_eq

added theorem Set.ncard_le_one_iff_subset_singleton

added theorem Set.ncard_le_one_of_subsingleton

added theorem Set.ncard_lt_ncard

added theorem Set.ncard_lt_ncard_iff_ncard_diff_lt_ncard_diff

added theorem Set.ncard_map

added theorem Set.ncard_mono

added theorem Set.ncard_ne_zero_of_mem

added theorem Set.ncard_pair

added theorem Set.ncard_pos

added theorem Set.ncard_preimage_ofInjective_subset_range

added theorem Set.ncard_singleton

added theorem Set.ncard_singleton_inter

added theorem Set.ncard_strictMono

added theorem Set.ncard_subtype

added theorem Set.ncard_union_add_ncard_inter

added theorem Set.ncard_union_eq

added theorem Set.ncard_union_le

added theorem Set.ncard_univ

added theorem Set.nonempty_of_ncard_ne_zero

added theorem Set.one_lt_ncard

added theorem Set.one_lt_ncard_iff

added theorem Set.pred_ncard_le_ncard_diff_singleton

added theorem Set.sep_of_ncard_eq

added theorem Set.subset_iff_eq_of_ncard_le

added theorem Set.surj_on_of_inj_on_of_ncard_le

added theorem Set.two_lt_ncard

added theorem Set.two_lt_ncard_iff