mem_commonNeighbors

Mathlib.Combinatorics.SimpleGraph.Basic

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

English

For any u, u belongs to the commonNeighbors of v and w iff u is adjacent to both v and w.

Русский

Для любых u верно: u ∈ общие соседи(v,w) тогда и только тогда, когда u смежно с v и u смежно с w.

LaTeX

$$$u \\in G.commonNeighbors(v,w) \\iff (G.Adj(v,u) \\wedge G.Adj(w,u))$$$

Lean4

theorem mem_commonNeighbors {u v w : V} : u ∈ G.commonNeighbors v w ↔ G.Adj v u ∧ G.Adj w u :=
  Iff.rfl

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

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

Разделы

Аффилиация

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