# Double countings #

This file gathers a few double counting arguments.

## Bipartite graphs #

In a bipartite graph (considered as a relation r : α → β → Prop), we can bound the number of edges between s : Finset α and t : Finset β by the minimum/maximum of edges over all a ∈ s times the size of s. Similarly for t. Combining those two yields inequalities between the sizes of s and t.

• bipartiteBelow: s.bipartiteBelow r b are the elements of s below b wrt to r. Its size is the number of edges of b in s.
• bipartiteAbove: t.bipartite_Above r a are the elements of t above a wrt to r. Its size is the number of edges of a in t.
• card_mul_le_card_mul, card_mul_le_card_mul': Double counting the edges of a bipartite graph from below and from above.
• card_mul_eq_card_mul: Equality combination of the previous.

### Bipartite graph #

def Finset.bipartiteBelow {α : Type u_1} {β : Type u_2} (r : αβProp) (s : ) (b : β) [(a : α) → Decidable (r a b)] :

Elements of s which are "below" b according to relation r.

Equations
Instances For
def Finset.bipartiteAbove {α : Type u_1} {β : Type u_2} (r : αβProp) (t : ) (a : α) [DecidablePred (r a)] :

Elements of t which are "above" a according to relation r.

Equations
Instances For
theorem Finset.bipartiteBelow_swap {α : Type u_1} {β : Type u_2} (r : αβProp) (t : ) (a : α) [DecidablePred (r a)] :
=
theorem Finset.bipartiteAbove_swap {α : Type u_1} {β : Type u_2} (r : αβProp) (s : ) (b : β) [(a : α) → Decidable (r a b)] :
=
@[simp]
theorem Finset.coe_bipartiteBelow {α : Type u_1} {β : Type u_2} (r : αβProp) (s : ) (b : β) [(a : α) → Decidable (r a b)] :
() = {a : α | a s r a b}
@[simp]
theorem Finset.coe_bipartiteAbove {α : Type u_1} {β : Type u_2} (r : αβProp) (t : ) (a : α) [DecidablePred (r a)] :
() = {b : β | b t r a b}
@[simp]
theorem Finset.mem_bipartiteBelow {α : Type u_1} {β : Type u_2} (r : αβProp) {s : } {b : β} [(a : α) → Decidable (r a b)] {a : α} :
a a s r a b
@[simp]
theorem Finset.mem_bipartiteAbove {α : Type u_1} {β : Type u_2} (r : αβProp) {t : } {a : α} [DecidablePred (r a)] {b : β} :
b b t r a b
theorem Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow {α : Type u_1} {β : Type u_2} (r : αβProp) {s : } {t : } [(a : α) → (b : β) → Decidable (r a b)] :
as, ().card = bt, ().card
theorem Finset.card_mul_le_card_mul {α : Type u_1} {β : Type u_2} (r : αβProp) {s : } {t : } {m : } {n : } [(a : α) → (b : β) → Decidable (r a b)] (hm : as, m ().card) (hn : bt, ().card n) :
s.card * m t.card * n

Double counting argument. Considering r as a bipartite graph, the LHS is a lower bound on the number of edges while the RHS is an upper bound.

theorem Finset.card_mul_le_card_mul' {α : Type u_1} {β : Type u_2} (r : αβProp) {s : } {t : } {m : } {n : } [(a : α) → (b : β) → Decidable (r a b)] (hn : bt, n ().card) (hm : as, ().card m) :
t.card * n s.card * m
theorem Finset.card_mul_eq_card_mul {α : Type u_1} {β : Type u_2} (r : αβProp) {s : } {t : } {m : } {n : } [(a : α) → (b : β) → Decidable (r a b)] (hm : as, ().card = m) (hn : bt, ().card = n) :
s.card * m = t.card * n
theorem Finset.card_le_card_of_forall_subsingleton {α : Type u_1} {β : Type u_2} (r : αβProp) {s : } {t : } (hs : as, bt, r a b) (ht : bt, {a : α | a s r a b}.Subsingleton) :
s.card t.card
theorem Finset.card_le_card_of_forall_subsingleton' {α : Type u_1} {β : Type u_2} (r : αβProp) {s : } {t : } (ht : bt, as, r a b) (hs : as, {b : β | b t r a b}.Subsingleton) :
t.card s.card
theorem Fintype.card_le_card_of_leftTotal_unique {α : Type u_1} {β : Type u_2} [] [] {r : αβProp} (h₁ : ) (h₂ : ) :
theorem Fintype.card_le_card_of_rightTotal_unique {α : Type u_1} {β : Type u_2} [] [] {r : αβProp} (h₁ : ) (h₂ : ) :