coe_adj_sub

Mathlib.Combinatorics.SimpleGraph.Subgraph

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

English

Adjacency in the subgraph coe corresponds to adjacency in the original subgraph.

Русский

Смежность в сопряженном подграфе соответствует смежности в исходном подграфе.

LaTeX

$$H.coe.Adj ⟨u,⋯⟩ ⟨v,⋯⟩ → H.Adj u v$$

Lean4

theorem coe_adj_sub (G' : Subgraph G) (u v : G'.verts) (h : G'.coe.Adj u v) : G.Adj u v :=
  G'.adj_sub h

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

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

Разделы

Аффилиация

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