English
See above
Русский
Пусть r — отношение между α и β, s ⊆ α, t ⊆ β; задающее двудольное соседство. Для любой функции f верны эквивалентные подсчеты сумм инцидентностей:
LaTeX
$$$$ \sum_{a \in s} \#(t.bipartiteAbove r a) = \sum_{b \in t} \#(s.bipartiteBelow r b) $$$$
Lean4
/-- **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 card_nsmul_le_card_nsmul [∀ a b, Decidable (r a b)] (hm : ∀ a ∈ s, m ≤ #(t.bipartiteAbove r a))
(hn : ∀ b ∈ t, #(s.bipartiteBelow r b) ≤ n) : #s • m ≤ #t • n :=
calc
_ ≤ ∑ a ∈ s, (#(t.bipartiteAbove r a) : R) := s.card_nsmul_le_sum _ _ hm
_ = ∑ b ∈ t, (#(s.bipartiteBelow r b) : R) := by norm_cast; rw [sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow]
_ ≤ _ := t.sum_le_card_nsmul _ _ hn
