neighborFinset_eq_filter

Mathlib.Combinatorics.SimpleGraph.Finite

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

English

The neighbor Finset of v equals the Finset of all w with G.Adj v w, i.e., the adjacent vertices.

Русский

Множество соседей v равно множество всех w, с которыми выполнено G.Adj v w.

LaTeX

$$G.neighborFinset v = Finset.filter (\lambda w, G.Adj v w) Finset.univ$$

Lean4

theorem neighborFinset_eq_filter {v : V} [DecidableRel G.Adj] : G.neighborFinset v = ({w | G.Adj v w} : Finset _) := by
  ext; simp

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

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

Разделы

Аффилиация

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