neighborSet_subset_support

Mathlib.Combinatorics.SimpleGraph.Basic

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

English

Every neighbor w of v is connected by an edge to v, hence {v,w} ∈ G.support.

Русский

Каждый сосед w вершины v образует ребро {v,w}, следовательно {v,w} ∈ поддержке графа.

LaTeX

$$$$ G.neighborSet(v) \subseteq G.support. $$$$

Lean4

theorem neighborSet_subset_support (v : V) : G.neighborSet v ⊆ G.support := fun _ hadj ↦ ⟨v, hadj.symm⟩

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

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

Разделы

Аффилиация

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