Commit 2023-01-20 14:41 75cca33f

View on Github →

feat port: Combinatorics.DoubleCounting (#1715)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/DoubleCounting.lean

added def Finset.bipartiteAbove

added theorem Finset.bipartiteAbove_swap

added def Finset.bipartiteBelow

added theorem Finset.bipartiteBelow_swap

added theorem Finset.card_le_card_of_forall_subsingleton'

added theorem Finset.card_le_card_of_forall_subsingleton

added theorem Finset.card_mul_eq_card_mul

added theorem Finset.card_mul_le_card_mul'

added theorem Finset.card_mul_le_card_mul

added theorem Finset.coe_bipartiteAbove

added theorem Finset.coe_bipartiteBelow

added theorem Finset.mem_bipartiteAbove

added theorem Finset.mem_bipartiteBelow

added theorem Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow

added theorem Fintype.card_le_card_of_leftTotal_unique

added theorem Fintype.card_le_card_of_rightTotal_unique