subgraph

Mathlib.Combinatorics.SimpleGraph.Acyclic

URI: https://scilib.ai/kg/mathlib#SimpleGraph.IsAcyclic.subgraph

← MathLib Explorer

English

A subgraph of an acyclic graph is acyclic.

Русский

Подграф ацикличного графа также ацикличен.

LaTeX

$$$G.IsAcyclic \Rightarrow \forall H: G.Subgraph, H.coe.IsAcyclic$$$

Lean4

/-- A subgraph of an acyclic graph is acyclic. -/
theorem subgraph (h : G.IsAcyclic) (H : G.Subgraph) : H.coe.IsAcyclic :=
  h.comap _ H.hom_injective

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

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

Разделы

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

Аффилиация

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