singletonSubgraph_snd_le_subgraphOfAdj

Mathlib.Combinatorics.SimpleGraph.Subgraph

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

English

If u is adjacent to v, then the singletonSubgraph at v is below the subgraphOfAdj hvw.

Русский

Если u смежна с v, то подграф-одиночка на v лежит ниже подграфа по hvw.

LaTeX

$$$\\text{singletonSubgraph}(v) \\le G.\\mathrm{subgraphOfAdj}(hvw)$$$

Lean4

theorem singletonSubgraph_snd_le_subgraphOfAdj {u v : V} {h : G.Adj u v} : G.singletonSubgraph v ≤ G.subgraphOfAdj h :=
  by simp

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

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

Разделы

Аффилиация

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