commonNeighbors_subset_neighborSet_left

Mathlib.Combinatorics.SimpleGraph.Basic

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

English

The set of common neighbors of v and w is contained in the neighbor set of v.

Русский

Множество общих соседей v и w есть подмножество множества соседей v.

LaTeX

$$$G.commonNeighbors(v,w) \\subseteq G.neighborSet(v)$$$

Lean4

theorem commonNeighbors_subset_neighborSet_left (v w : V) : G.commonNeighbors v w ⊆ G.neighborSet v :=
  Set.inter_subset_left

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

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

Разделы

Аффилиация

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