mem_supp_of_adj_mem_supp

Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

URI: https://scilib.ai/kg/mathlib#SimpleGraph.ConnectedComponent.mem_supp_of_adj_mem_supp

← MathLib Explorer

English

If u is in the support of C and u is adjacent to v, then v lies in the support of C as well.

Русский

Если u ∈ C.supp и u сосед ∈ v, тогда и v ∈ C.supp.

LaTeX

$$$u \\\\in C.supp \\\\land G.Adj u v \\\\Rightarrow v \\\\in C.supp$$$

Lean4

theorem mem_supp_of_adj_mem_supp {G : SimpleGraph V} (C : G.ConnectedComponent) {u v : V} (hu : u ∈ C.supp)
    (hadj : G.Adj u v) : v ∈ C.supp :=
  (mem_supp_congr_adj C hadj).mp hu

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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