commonNeighbors_subset_neighborSet_right

Mathlib.Combinatorics.SimpleGraph.Basic

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

English

Similarly, CN(v,w) ⊆ N(w).

Русский

Аналогично, CN(v,w) ⊆ N(w).

LaTeX

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

Lean4

theorem commonNeighbors_subset_neighborSet_right (v w : V) : G.commonNeighbors v w ⊆ G.neighborSet w :=
  Set.inter_subset_right

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

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

Разделы

Аффилиация

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