card_mul_le_card_mul' — Mathlib

English

A variant of the product bound using swapped roles in the bipartite incidence setup.

Русский

Вариант ограничение на произведение с перестановкой ролей во взаимосвязи между двумя частями графа.

LaTeX

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

Lean4

theorem card_mul_le_card_mul' [∀ 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' _ hn hm

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