Commit 2023-01-28 07:25 609e73bc

View on Github →

feat: port Data.PNat.Interval (#1894)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/PNat/Interval.lean

added theorem PNat.Icc_eq_finset_subtype

added theorem PNat.Ico_eq_finset_subtype

added theorem PNat.Ioc_eq_finset_subtype

added theorem PNat.Ioo_eq_finset_subtype

added theorem PNat.card_Icc

added theorem PNat.card_Ico

added theorem PNat.card_Ioc

added theorem PNat.card_Ioo

added theorem PNat.card_fintype_Icc

added theorem PNat.card_fintype_Ico

added theorem PNat.card_fintype_Ioc

added theorem PNat.card_fintype_Ioo

added theorem PNat.map_subtype_embedding_Icc

added theorem PNat.map_subtype_embedding_Ico

added theorem PNat.map_subtype_embedding_Ioc

added theorem PNat.map_subtype_embedding_Ioo