spanningCoe_subgraphOfAdj

Mathlib.Combinatorics.SimpleGraph.Subgraph

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

← MathLib Explorer

English

For a spanning subgraph G', spanningCoe is isomorphic to coe: G'.spanningCoe ≃g G'.coe.

Русский

Для растягивающего подграфа G' spanningCoe эквивалентно coe: G'.spanningCoe ≃g G'.coe.

LaTeX

$$G'.spanningCoe ≃g G'.coe$$

Lean4

@[simp]
theorem spanningCoe_subgraphOfAdj {v w : V} (hadj : G.Adj v w) :
    (G.subgraphOfAdj hadj).spanningCoe = fromEdgeSet {s(v, w)} :=
  by
  ext v w
  aesop

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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