Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-30 14:54 11de8674

View on Github →

feat(data/fin/interval): add lemmas (#11102) From flt-regular.

Estimated changes

Modified src/data/fin/basic.lean

added theorem fin.bot_eq_zero

added theorem fin.top_eq_last

Modified src/data/fin/interval.lean

added theorem fin.card_filter_ge

added theorem fin.card_filter_gt

added theorem fin.card_filter_le

added theorem fin.card_filter_le_le

added theorem fin.card_filter_le_lt

added theorem fin.card_filter_lt

added theorem fin.card_filter_lt_le

added theorem fin.card_filter_lt_lt

Modified src/data/finset/locally_finite.lean

added theorem finset.filter_ge_eq_Iic

added theorem finset.filter_gt_eq_Iio

added theorem finset.filter_le_eq_Ici

added theorem finset.filter_le_le_eq_Icc

added theorem finset.filter_le_lt_eq_Ico

added theorem finset.filter_lt_eq_Ioi

added theorem finset.filter_lt_le_eq_Ioc

added theorem finset.filter_lt_lt_eq_Ioo