induce_verts

Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Subgraph.Connected.induce_verts

Lean4

theorem induce_verts {H : G.Subgraph} (h : H.Connected) : (G.induce H.verts).Connected :=
  by
  rw [connected_induce_iff]
  exact h.mono le_induce_top_verts (by exact rfl)

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

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

Разделы

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

Аффилиация

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