card_nsmul_le_card_nsmul' — Mathlib

English

Under the same double counting framework, there is a symmetrical bound: #t · n ≤ #s · m whenever the bipartite neighborhood sizes satisfy the corresponding bounds with roles swapped.

Русский

В рамках одинакового двойного подсчета существует симметричная неравенство: |t|·n ≤ |s|·m при соответствующих ограничениях на размеры окрестностей с перестановкой ролей.

LaTeX

$$$$ \#t \cdot n \le \#s \cdot m $$$$

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

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