isTree_iff_minimal_connected — Mathlib

English

A graph is a tree iff it is minimally connected.

Русский

Граф является деревом тогда и только тогда, когда он минимально связан.

LaTeX

$$$IsTree\ G \iff Minimal\ Connected\ G$$$

Lean4

theorem isTree_iff_minimal_connected : IsTree G ↔ Minimal Connected G :=
  by
  refine ⟨fun htree ↦ ⟨htree.isConnected, fun G' h' hle u v hadj ↦ ?_⟩, isTree_of_minimal_connected⟩
  have ⟨p, hp⟩ := h'.exists_isPath u v
  have :=
    congrArg Walk.edges <|
      congrArg Subtype.val <| htree.IsAcyclic.path_unique ⟨p.mapLe hle, hp.mapLe hle⟩ <| Path.singleton hadj
  simp only [edges_map, Hom.coe_ofLE, Sym2.map_id, List.map_id_fun, id_eq] at this
  simp [this, p.adj_of_mem_edges]

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