card_interedges_le_mul

Mathlib.Combinatorics.SimpleGraph.Density

URI: https://scilib.ai/kg/mathlib#SimpleGraph.card_interedges_le_mul

English

The number of interedges between s and t does not exceed |s| · |t|.

Русский

Число межрёбер между s и t не превосходит |s| · |t|.

LaTeX

$$#(G.interedges s t) ≤ #s * #t$$

Lean4

theorem card_interedges_le_mul (s t : Finset α) : #(G.interedges s t) ≤ #s * #t :=
  Rel.card_interedges_le_mul _ _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru