English
If s is nonempty and the lower bound m on the left-hand side is strictly less than the bipartite neighborhood sizes, while the right-hand side upper bound n is at least as large as the corresponding sizes, then #s · m < #t · n.
Русский
Если s непусто и нижняя граница m слева строго меньше размеров окрестностей bipartite, а правая верхняя граница 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 strict lower bound on the number of edges while
the RHS is an upper bound. -/
theorem card_nsmul_lt_card_nsmul_of_lt_of_le [∀ a b, Decidable (r a b)] (hs : s.Nonempty)
(hm : ∀ a ∈ s, m < #(t.bipartiteAbove r a)) (hn : ∀ b ∈ t, #(s.bipartiteBelow r b) ≤ n) : #s • m < #t • n :=
calc
_ = ∑ _a ∈ s, m := by rw [sum_const]
_ < ∑ a ∈ s, (#(t.bipartiteAbove r a) : R) := (sum_lt_sum_of_nonempty hs 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
