anti

Mathlib.Combinatorics.SimpleGraph.Acyclic

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

← MathLib Explorer

English

A spanning subgraph of an acyclic graph is acyclic.

Русский

Расширенный подграф ацикличного графа является ацикличным.

LaTeX

$$$G \le G' \Rightarrow G'.IsAcyclic \Rightarrow G.IsAcyclic$$$

Lean4

/-- A spanning subgraph of an acyclic graph is acyclic. -/
theorem anti {G' : SimpleGraph V} (hsub : G ≤ G') (h : G'.IsAcyclic) : G.IsAcyclic :=
  h.comap ⟨_, fun h ↦ hsub h⟩ Function.injective_id

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

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

Разделы

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

Аффилиация

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