of_comap

Mathlib.Combinatorics.SimpleGraph.Acyclic

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

English

If G is acyclic and f is an embedding V' ↪ V, then the comap of G along f is acyclic.

Русский

Если граф G ацикличен и f: V' ↪ V является вложением, то граф comap f(G) ацикличен.

LaTeX

$$$\forall f: V' \hookrightarrow V,\ G.IsAcyclic \Rightarrow (G.comap f).IsAcyclic$$$

Lean4

theorem of_comap (f : V' ↪ V) (h : G.IsAcyclic) : G.comap f |>.IsAcyclic :=
  h.embedding <| SimpleGraph.Embedding.comap ..

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

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

Разделы

Аффилиация

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