Commit 2023-06-26 11:35 3ff3f2d6

View on Github →

feat(set_theory/cardinal/finite): prove lemmas to handle part_enat.card (#19198) Prove some lemmas that allow to handle part_enat.card of finite cardinals, analogous to those about nat.card

Estimated changes

Modified src/data/finite/card.lean

added theorem part_enat.card_eq_coe_nat_card

Modified src/data/nat/part_enat.lean

added theorem part_enat.coe_succ_le_iff

added theorem part_enat.lt_coe_succ_iff_le

Modified src/set_theory/cardinal/basic.lean

modified theorem cardinal.sum_lt_prod

added theorem cardinal.to_nat_eq_iff_eq_of_lt_aleph_0

added theorem cardinal.to_part_enat_congr

added theorem cardinal.to_part_enat_eq_iff_eq_of_le_aleph_0

added theorem cardinal.to_part_enat_eq_top_iff_le_aleph_0

added theorem cardinal.to_part_enat_le_iff_le_of_le_aleph_0

added theorem cardinal.to_part_enat_le_iff_le_of_lt_aleph_0

added theorem cardinal.to_part_enat_lift

added theorem cardinal.to_part_enat_mono

Modified src/set_theory/cardinal/finite.lean

added theorem cardinal.coe_nat_eq_to_part_enat_iff

added theorem cardinal.coe_nat_le_to_part_enat_iff

added theorem cardinal.coe_nat_lt_coe_iff_lt

added theorem cardinal.lt_coe_nat_iff_lt

added theorem cardinal.to_part_enat_eq_coe_nat_iff

added theorem cardinal.to_part_enat_le_coe_nat_iff

added theorem part_enat.card_congr

added theorem part_enat.card_eq_zero_iff_empty

added theorem part_enat.card_image_of_inj_on

added theorem part_enat.card_image_of_injective

added theorem part_enat.card_le_one_iff_subsingleton

added theorem part_enat.card_plift

added theorem part_enat.card_ulift

added theorem part_enat.is_finite_of_card

added theorem part_enat.one_lt_card_iff_nontrivial