notMem_neighborFinset_self

Mathlib.Combinatorics.SimpleGraph.Finite

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

English

A vertex is not adjacent to itself, hence v is not a member of its own neighborFinset.

Русский

Вершина не смежна сама с собой, следовательно v не принадлежит своему neighborFinset.

LaTeX

$$$ v \notin G.neighborFinset v $$$

Lean4

theorem notMem_neighborFinset_self : v ∉ G.neighborFinset v := by simp

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

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

Разделы

Аффилиация

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