card_nsmul_lt_card_nsmul_of_lt_of_le'

English

A variant of the double counting argument where a strict inequality is permitted in counting certain edge occurrences, leading to a strict bound on the product of set sizes.

Русский

Вариант двойного подсчета, допускающий строгую неравенство при подсчете определённых рёбер, что даёт строгое ограничение на произведение кардиналей множеств.

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)] (ht : t.Nonempty)
    (hn : ∀ b ∈ t, n < #(s.bipartiteBelow r b)) (hm : ∀ a ∈ s, #(t.bipartiteAbove r a) ≤ m) : #t • n < #s • m :=
  card_nsmul_lt_card_nsmul_of_lt_of_le (swap r) ht hn hm

Похожие утверждения