isTree_iff_existsUnique_path — 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 isTree_iff_existsUnique_path : G.IsTree ↔ Nonempty V ∧ ∀ v w : V, ∃! p : G.Walk v w, p.IsPath := by
  classical
  rw [isTree_iff, isAcyclic_iff_path_unique]
  constructor
  · rintro ⟨hc, hu⟩
    refine ⟨hc.nonempty, ?_⟩
    intro v w
    let q := (hc v w).some.toPath
    use q
    simp only [true_and, Path.isPath]
    intro p hp
    specialize hu ⟨p, hp⟩ q
    exact Subtype.ext_iff.mp hu
  · rintro ⟨hV, h⟩
    refine ⟨Connected.mk ?_, ?_⟩
    · intro v w
      obtain ⟨p, _⟩ := h v w
      exact p.reachable
    · rintro v w ⟨p, hp⟩ ⟨q, hq⟩
      simp only [ExistsUnique.unique (h v w) hp hq]

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