Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-04 22:36 b064622f

View on Github →

feat(data/fin/interval): Cardinality of finset.Ixi/finset.Iix in fin (#10168) This proves (Ici a).card = n + 1 - a, (Ioi a).card = n - a, (Iic b).card = b + 1, (Iio b).card = b where a b : fin (n + 1) (and also a b : ℕ for the last two).

Estimated changes

Modified src/data/fin/interval.lean

added theorem fin.Ici_eq_finset_subtype

added theorem fin.Iic_eq_finset_subtype

added theorem fin.Iio_eq_finset_subtype

added theorem fin.Ioi_eq_finset_subtype

added theorem fin.card_Ici

added theorem fin.card_Iic

added theorem fin.card_Iio

added theorem fin.card_Ioi

added theorem fin.card_fintype_Ici

added theorem fin.card_fintype_Iic

added theorem fin.card_fintype_Iio

added theorem fin.card_fintype_Ioi

added theorem fin.map_subtype_embedding_Ici

added theorem fin.map_subtype_embedding_Iic

added theorem fin.map_subtype_embedding_Iio

added theorem fin.map_subtype_embedding_Ioi

Modified src/data/nat/interval.lean

added theorem nat.card_Iic

added theorem nat.card_Iio

added theorem nat.card_fintype_Iic

added theorem nat.card_fintype_Iio