induce_pair_connected_of_adj

Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

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

← MathLib Explorer

English

If two vertices u and v are adjacent, the induced subgraph on {u, v} is connected.

Русский

Если вершины u и v смежны, индукцированный по {u, v} подграф связен.

LaTeX

$$(G.Adj u v) → (G.induce {u,v}).Connected$$

Lean4

theorem induce_pair_connected_of_adj {u v : V} (huv : G.Adj u v) : (G.induce { u, v }).Connected :=
  by
  rw [connected_induce_iff]
  exact Subgraph.top_induce_pair_connected_of_adj huv

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

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

Разделы

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

Аффилиация

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