interedges_def

Mathlib.Combinatorics.SimpleGraph.Density

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

English

For a graph G, the interedges between two vertex-sets s and t are exactly the pairs from s×t that are adjacent in G.

Русский

Для графа G ребра между множествами вершин s и t — это пары из s×t, которые смежны в G.

LaTeX

$$$G\,\text{interedges}(s,t) = \{(x,y)\in s\times t : G.Adj(x,y)\}$$$

Lean4

theorem interedges_def (s t : Finset α) : G.interedges s t = {e ∈ s ×ˢ t | G.Adj e.1 e.2} :=
  rfl

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

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

Разделы

Аффилиация

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