of_map

Mathlib.Combinatorics.SimpleGraph.Acyclic

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

English

If the image of G under an embedding f is acyclic, then G itself is acyclic.

Русский

Если образ графа G под вложением f ацикличен, то сам граф G также ацикличен.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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