Finset.card_mul_le_card_mul

theorem Finset.card_mul_le_card_mul : ∀ {α : Type u_1} {β : Type u_2} (r : α → β → Prop) {s : Finset α} {t : Finset β} {m n : ℕ} [inst : (a : α) → (b : β) → Decidable (r a b)], (∀ a ∈ s, m ≤ (Finset.bipartiteAbove r t a).card) → (∀ b ∈ t, (Finset.bipartiteBelow r s b).card ≤ n) → s.card * m ≤ t.card * n

This theorem, known as the "Double counting argument", concerns a bipartite relation `r` between elements of two types `α` and `β`. Given finite sets `s` and `t` of these types and integers `m` and `n`, it asserts that if every element `a` in `s` is related to at least `m` elements in `t` and every element `b` in `t` is related to at most `n` elements in `s`, then the size of `s` multiplied by `m` is less than or equal to the size of `t` multiplied by `n`. In terms of graph theory, this can be conceptualized by interpreting `r` as a bipartite graph, where the left-hand side (`s.card * m`) provides a lower bound on the number of edges, and the right-hand side (`t.card * n`) provides an upper bound.

More concisely: If every element in a finite set of type `α` is related to at least `m` elements in a finite set of type `β`, and every element in the set of type `β` is related to at most `n` elements in the set of type `α`, then the product of the sizes of the sets and their respective bounds on the number of relations satisfies `(size s * m) <= (size t * n)`.