isAcyclic_of_path_unique — Mathlib

English

A graph is a tree iff there exists a unique path between any two vertices.

Русский

Граф является деревом тогда и только тогда, когда между любой парой вершин существует единственный путь.

LaTeX

$$$G.IsTree \iff (Nonempty V \land ∀ v w: V, ∃! p: G.Walk v w, p.IsPath)$$$

Lean4

theorem isAcyclic_of_path_unique (h : ∀ (v w : V) (p q : G.Path v w), p = q) : G.IsAcyclic :=
  by
  intro v c hc
  simp only [Walk.isCycle_def, Ne] at hc
  cases c with
  | nil => cases hc.2.1 rfl
  | cons ha c' =>
    simp only [Walk.cons_isTrail_iff, Walk.support_cons, List.tail_cons] at hc
    specialize h _ _ ⟨c', by simp only [Walk.isPath_def, hc.2]⟩ (Path.singleton ha.symm)
    rw [Path.singleton, Subtype.mk.injEq] at h
    simp [h] at hc

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