card_mul_le_card_mul — Mathlib

English

A basic consequence of double counting: the product of the cardinalities of two parts bounds the product of the counts in the opposite order.

Русский

Основной вывод из двойного подсчета: произведение кардиналитетов двух частей ограничивает произведение подсчетов в обратном порядке.

LaTeX

$$$$ #s \cdot m \le #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 an upper bound. -/
theorem card_mul_le_card_mul [∀ 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 :=
  card_nsmul_le_card_nsmul _ hm hn

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