isAcyclic_iff_path_unique

Mathlib.Combinatorics.SimpleGraph.Acyclic

URI: https://scilib.ai/kg/mathlib#SimpleGraph.isAcyclic_iff_path_unique

English

If path uniqueness holds for all vertex pairs, then the graph is acyclic.

Русский

Если для всех пар вершин пути уникальны, граф ацикличесен.

LaTeX

$$$(\forall v w, \forall p q: G.Path v w, p = q) \Rightarrow G.IsAcyclic$$$

Lean4

theorem isAcyclic_iff_path_unique : G.IsAcyclic ↔ ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q :=
  ⟨IsAcyclic.path_unique, isAcyclic_of_path_unique⟩

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

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

Разделы

Аффилиация

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