Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-30 14:04 74c2af38

View on Github →

feat(data/set/ncard): noncomputable set cardinality (#18576) This PR introduces a function set.ncard that (noncomputably) gives the cardinality of a finite set, or zero if the set is infinite. The intention is to give a way to reason about set cardinality that avoids data and going between set and finset. This is especially useful for reasoning about sets in a finite type. The added file is somewhat large, but it is essentially just duplicating the API in data.finset.card (minus the induction lemmas).

Estimated changes

added theorem set.exists_smaller_set
added theorem set.infinite.ncard
added theorem set.le_ncard_diff
added theorem set.map_eq_of_subset
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_empty
added theorem set.ncard_eq_one
added theorem set.ncard_eq_succ
added theorem set.ncard_eq_three
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_insert_le
added theorem set.ncard_le_of_subset
added theorem set.ncard_le_one
added theorem set.ncard_le_one_iff
added theorem set.ncard_lt_ncard
added theorem set.ncard_map
added theorem set.ncard_mono
added theorem set.ncard_pair
added theorem set.ncard_pos
added theorem set.ncard_singleton
added theorem set.ncard_strict_mono
added theorem set.ncard_subtype
added theorem set.ncard_union_eq
added theorem set.ncard_union_le
added theorem set.ncard_univ
added theorem set.one_lt_ncard
added theorem set.one_lt_ncard_iff
added theorem set.sep_of_ncard_eq
added theorem set.two_lt_card
added theorem set.two_lt_ncard_iff