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]