connected_toSimpleGraph

Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

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

← MathLib Explorer

English

The induced subgraph on a connected component is connected.

Русский

Порожденный подпgraph на компоненте связности является связным.

LaTeX

$$$ (C.toSimpleGraph).Connected $$$

Lean4

theorem connected_toSimpleGraph (C : ConnectedComponent G) : (C.toSimpleGraph).Connected
    where
  preconnected := by
    intro ⟨u, hu⟩ ⟨v, hv⟩
    exact C.reachable_toSimpleGraph hu hv
  nonempty := ⟨C.out, C.out_eq⟩

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

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

Разделы

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

Аффилиация

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