Commit 2023-06-26 11:36 9f3a6c79

View on Github →

feat(SetTheory/Cardinal/Finite): prove lemmas about PartENat.card (#5307) Prove lemmas to handle PartENat.card Inspired from the similar lemmas for Nat.card This is a mathlib4 companion to the PR #19198 of mathlib3

Estimated changes

Modified Mathlib/Data/Finite/Card.lean

added theorem PartENat.card_eq_coe_nat_card

Modified Mathlib/Data/Nat/PartENat.lean

added theorem PartENat.coe_succ_le_iff

added theorem PartENat.lt_coe_succ_iff_le

Modified Mathlib/SetTheory/Cardinal/Basic.lean

added theorem Cardinal.toNat_eq_iff_eq_of_lt_aleph0

added theorem Cardinal.toPartENat_congr

added theorem Cardinal.toPartENat_eq_iff_of_le_aleph0

added theorem Cardinal.toPartENat_eq_top_iff_le_aleph0

added theorem Cardinal.toPartENat_le_iff_of_le_aleph0

added theorem Cardinal.toPartENat_le_iff_of_lt_aleph0

added theorem Cardinal.toPartENat_lift

added theorem Cardinal.toPartENat_mono

Modified Mathlib/SetTheory/Cardinal/Finite.lean

added theorem Cardinal.natCast_eq_toPartENat_iff

added theorem Cardinal.natCast_le_toPartENat_iff

added theorem Cardinal.natCast_lt_toPartENat_iff

added theorem Cardinal.toPartENat_eq_natCast_iff

added theorem Cardinal.toPartENat_le_natCast_iff

added theorem Cardinal.toPartENat_lt_natCast_iff

added theorem PartENat.card_congr

added theorem PartENat.card_eq_zero_iff_empty

added theorem PartENat.card_image_of_injOn

added theorem PartENat.card_image_of_injective

added theorem PartENat.card_le_one_iff_subsingleton

added theorem PartENat.card_pLift

added theorem PartENat.card_uLift

added theorem PartENat.one_lt_card_iff_nontrivial