Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-26 00:12 b8c3e61b

View on Github →

refactor(*): Use finset.Iix/finset.Ixi (#14448) Now that finset.Iix/finset.Ixi work for empty types, there is no need for univ.filter (λ j, j < i) and similar.

Estimated changes

added theorem fin.prod_Ioi_succ
added theorem fin.prod_Ioi_zero
deleted theorem fin.prod_filter_succ_lt
deleted theorem fin.prod_filter_zero_lt
deleted theorem fin.card_filter_ge
deleted theorem fin.card_filter_gt
deleted theorem fin.card_filter_le
deleted theorem fin.card_filter_le_le
deleted theorem fin.card_filter_le_lt
deleted theorem fin.card_filter_lt
deleted theorem fin.card_filter_lt_le
deleted theorem fin.card_filter_lt_lt
modified theorem finset.disjoint_left
modified theorem finset.disjoint_right
added theorem fin.Ioi_succ
added theorem fin.Ioi_zero_eq_map
deleted theorem fin.univ_filter_succ_lt
deleted theorem fin.univ_filter_zero_lt