existsUnique_path

Mathlib.Combinatorics.SimpleGraph.Acyclic

URI: https://scilib.ai/kg/mathlib#SimpleGraph.IsTree.existsUnique_path

English

From a tree, there exists a unique path between any two vertices.

Русский

Из дерева существует уникальный путь между любой парой вершин.

LaTeX

$$$G.IsTree \Rightarrow ∀ v w: V, ∃! p: G.Walk v w, p.IsPath$$$

Lean4

theorem existsUnique_path (hG : G.IsTree) : ∀ v w, ∃! p : G.Walk v w, p.IsPath :=
  (isTree_iff_existsUnique_path.1 hG).2

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

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

Разделы

Аффилиация

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