mem_neighborFinset

Mathlib.Combinatorics.SimpleGraph.Finite

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

English

w is a neighbor of v if and only if w belongs to the Finset of neighbors of v.

Русский

w является соседом v тогда и только тогда, когда w принадлежит Finset соседей v.

LaTeX

$$$ w \in G.neighborFinset v \iff G.Adj v w $$$

Lean4

@[simp]
theorem mem_neighborFinset (w : V) : w ∈ G.neighborFinset v ↔ G.Adj v w :=
  Set.mem_toFinset

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

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

Разделы

Аффилиация

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