neighborSet_subgraphOfAdj_of_ne_of_ne

Mathlib.Combinatorics.SimpleGraph.Subgraph

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

← MathLib Explorer

English

The neighbor set at w in the subgraphOfAdj hvw is exactly {v}.

Русский

Множество соседей вершины w в подграфе по hvw равно {v}.

LaTeX

$$$(G.\\mathrm{subgraphOfAdj}(hvw).\\mathrm{neighborSet}(w) = \\{ v \\}$$$

Lean4

@[simp]
theorem neighborSet_subgraphOfAdj_of_ne_of_ne {u v w : V} (hvw : G.Adj v w) (hv : u ≠ v) (hw : u ≠ w) :
    (G.subgraphOfAdj hvw).neighborSet u = ∅ := by
  ext
  simp [hv.symm, hw.symm]

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

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

Разделы

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

Аффилиация

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