English
In the double counting setting, if the left lower bound is bounded above by m and the right upper bound is bounded below by n, then #s · m < #t · n.
Русский
В рамках двойного подсчета, если левая нижняя граница ≤ m, правая верхняя граница ≥ n, то #s · m < #t · n.
LaTeX
$$$$ \#s \cdot m < \#t \cdot n $$$$
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 a strict upper bound. -/
theorem card_nsmul_lt_card_nsmul_of_le_of_lt [∀ a b, Decidable (r a b)] (ht : t.Nonempty)
(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]
_ < ∑ _b ∈ t, n := (sum_lt_sum_of_nonempty ht hn)
_ = _ := sum_const _
