Commit 2023-01-23 12:37 5742ec16

View on Github →

feat: Port Combinatorics.Pigeonhole (#1758)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/Pigeonhole.lean

added theorem Finset.exists_card_fiber_le_of_card_le_mul

added theorem Finset.exists_card_fiber_le_of_card_le_nsmul

added theorem Finset.exists_card_fiber_lt_of_card_lt_mul

added theorem Finset.exists_card_fiber_lt_of_card_lt_nsmul

added theorem Finset.exists_le_card_fiber_of_mul_le_card_of_maps_to

added theorem Finset.exists_le_card_fiber_of_nsmul_le_card_of_maps_to

added theorem Finset.exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum

added theorem Finset.exists_le_sum_fiber_of_sum_fiber_nonpos_of_nsmul_le_sum

added theorem Finset.exists_lt_card_fiber_of_mul_lt_card_of_maps_to

added theorem Finset.exists_lt_card_fiber_of_nsmul_lt_card_of_maps_to

added theorem Finset.exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum

added theorem Finset.exists_lt_sum_fiber_of_sum_fiber_nonpos_of_nsmul_lt_sum

added theorem Finset.exists_sum_fiber_le_of_maps_to_of_sum_le_nsmul

added theorem Finset.exists_sum_fiber_le_of_sum_fiber_nonneg_of_sum_le_nsmul

added theorem Finset.exists_sum_fiber_lt_of_maps_to_of_sum_lt_nsmul

added theorem Finset.exists_sum_fiber_lt_of_sum_fiber_nonneg_of_sum_lt_nsmul

added theorem Fintype.exists_card_fiber_le_of_card_le_mul

added theorem Fintype.exists_card_fiber_le_of_card_le_nsmul

added theorem Fintype.exists_card_fiber_lt_of_card_lt_mul

added theorem Fintype.exists_card_fiber_lt_of_card_lt_nsmul

added theorem Fintype.exists_le_card_fiber_of_mul_le_card

added theorem Fintype.exists_le_card_fiber_of_nsmul_le_card

added theorem Fintype.exists_le_sum_fiber_of_nsmul_le_sum

added theorem Fintype.exists_lt_card_fiber_of_mul_lt_card

added theorem Fintype.exists_lt_card_fiber_of_nsmul_lt_card

added theorem Fintype.exists_lt_sum_fiber_of_nsmul_lt_sum

added theorem Fintype.exists_sum_fiber_le_of_sum_le_nsmul

added theorem Fintype.exists_sum_fiber_lt_of_sum_lt_nsmul

added theorem Nat.exists_lt_modEq_of_infinite