Commit 2022-01-11 20:49 8db96a8f

feat(combinatorics/double_counting): Double-counting the edges of a bipartite graph (#11372) This proves a classic of double-counting arguments: If each element of the |α| elements on the left is connected to at least m elements on the right and each of the |β| elements on the right is connected to at most n elements on the left, then |α| * m ≤ |β| * n because the LHS is less than the number of edges which is less than the RHS. This is put in a new file combinatorics.double_counting with the idea that we could gather double counting arguments here, much as is done with combinatorics.pigeonhole.