Commit 2024-12-01 00:08 fa4bdc15

View on Github →

feat: introduce ENat.card, and use it in place of PartENat.card (#19624)

Estimated changes

Modified Mathlib/Algebra/Group/Pointwise/Set/Card.lean

modified theorem Set.encard_inv

Modified Mathlib/Analysis/Convex/Radon.lean

Modified Mathlib/Data/Finite/Card.lean

added theorem ENat.card_eq_coe_natCard

Modified Mathlib/Data/Set/Card.lean

Modified Mathlib/SetTheory/Cardinal/ENat.lean

added theorem Cardinal.toENat_congr

added theorem Cardinal.toENat_eq_iff_of_le_aleph0

added theorem Cardinal.toENat_le_iff_of_le_aleph0

added theorem Cardinal.toENat_le_iff_of_lt_aleph0

Modified Mathlib/SetTheory/Cardinal/Finite.lean

added theorem Cardinal.natCast_eq_toENat_iff

added theorem Cardinal.natCast_le_toENat_iff

added theorem Cardinal.natCast_lt_toENat_iff

added theorem Cardinal.toENat_eq_natCast_iff

added theorem Cardinal.toENat_le_natCast_iff

added theorem Cardinal.toENat_lt_natCast_iff

added def ENat.card

added theorem ENat.card_congr

added theorem ENat.card_eq_coe_fintype_card

added theorem ENat.card_eq_top_of_infinite

added theorem ENat.card_eq_zero_iff_empty

added theorem ENat.card_image_of_injOn

added theorem ENat.card_image_of_injective

added theorem ENat.card_le_one_iff_subsingleton

added theorem ENat.card_plift

added theorem ENat.card_sum

added theorem ENat.card_ulift

added theorem ENat.one_lt_card_iff_nontrivial

modified theorem PartENat.card_plift

modified theorem PartENat.card_ulift