card_nsmul_lt_card_nsmul_of_le_of_lt'

English

A symmetric variant of the double counting lemma comparing the sizes of neighborhoods across the two parts of the bipartite relation.

Русский

Симметричный вариант леммы двойного подсчета, сопоставляющий размеры окрестностей между двумя частями двудольного отношения.

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 a strict upper bound. -/
theorem card_nsmul_lt_card_nsmul_of_le_of_lt' [∀ a b, Decidable (r a b)] (hs : s.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_le_of_lt (swap r) hs hn hm

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