Commit 2023-08-02 02:18 444b9f33

View on Github →

feat(Data.Set.Ncard): enat set cardinality (#5908) This PR is a second attempt at defining the cardinality of a set as extended natural number, with a function encard. The implementation involves a refactor, where the existingncard function is redefined in terms of encard. This shortens a lot of proofs, reduces reliance on the Finset API, and allows for a potential future refactor where ncard is removed if it is decided to be redundant.

Estimated changes

added theorem ENat.le_coe_iff
added theorem Set.Infinite.encard_eq
modified theorem Set.Infinite.ncard
added theorem Set.InjOn.encard_image
added theorem Set.Nat.encard_range
added theorem Set.encard_congr
added theorem Set.encard_empty
added theorem Set.encard_eq_one
added theorem Set.encard_eq_three
added theorem Set.encard_eq_top_iff
added theorem Set.encard_eq_two
added theorem Set.encard_eq_zero
added theorem Set.encard_exchange'
added theorem Set.encard_exchange
added theorem Set.encard_image_le
added theorem Set.encard_insert_le
added theorem Set.encard_le_coe_iff
added theorem Set.encard_le_one_iff
added theorem Set.encard_lt_top_iff
added theorem Set.encard_mono
added theorem Set.encard_ne_top_iff
added theorem Set.encard_ne_zero
added theorem Set.encard_pair
added theorem Set.encard_pos
added theorem Set.encard_singleton
added theorem Set.encard_strictMono
added theorem Set.encard_union_eq
added theorem Set.encard_union_le
added theorem Set.encard_univ
added theorem Set.encard_univ_coe
modified theorem Set.ncard_def
modified theorem Set.ncard_exchange
modified theorem Set.ncard_image_of_injOn
modified theorem Set.ncard_insert_of_mem
modified theorem Set.ncard_singleton_inter
added theorem Set.one_lt_encard_iff
added theorem PartENat.card_sum