componentComplMk_mem

Mathlib.Combinatorics.SimpleGraph.Ends.Defs

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

English

For any G, v outside K belongs to G.componentComplMk vK.

Русский

Для любого G верши́на вне K принадлежит компоненте G.componentComplMk vK.

LaTeX

$$$$ \text{componentComplMk}(G, vK) \text{ contains } v $$$$

Lean4

theorem componentComplMk_mem (G : SimpleGraph V) {v : V} (vK : v ∉ K) : v ∈ G.componentComplMk vK :=
  ⟨vK, rfl⟩

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

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

Разделы

Аффилиация

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