of_spanningCoe

Mathlib.Combinatorics.SimpleGraph.Subgraph

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Subgraph.Adj.of_spanningCoe

English

If G' is a subgraph of G and u,v are vertices of G', any edge in spanningCoe corresponds to an edge in G.

Русский

Если G' — подграф G и u,v — вершины G', ребро в spanningCoe соответствует ребру в G.

LaTeX

$$if h : G'.spanningCoe.Adj u v then G.Adj u v$$

Lean4

theorem of_spanningCoe {G' : Subgraph G} {u v : G'.verts} (h : G'.spanningCoe.Adj u v) : G.Adj u v :=
  G'.adj_sub h

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

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

Разделы

Аффилиация

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