card_interedges_le_mul — Mathlib

English

The number of edges between finite sets s and t is at most the product of their sizes.

Русский

Число ребер между конечными множествами s и t не превосходит произведения их объёмов.

LaTeX

$$$\#\operatorname{interedges}(r, s, t) \le |s| \cdot |t|$$$

Lean4

theorem card_interedges_le_mul (s : Finset α) (t : Finset β) : #(interedges r s t) ≤ #s * #t :=
  (card_filter_le _ _).trans (card_product _ _).le

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