isTree_of_minimal_connected — Mathlib

English

A minimally connected graph is a tree.

Русский

Минимально связный граф является деревом.

LaTeX

$$$Minimal\ Connected\ G \Rightarrow IsTree\ G$$$

Lean4

/-- A minimally connected graph is a tree. -/
theorem isTree_of_minimal_connected (h : Minimal Connected G) : IsTree G :=
  by
  rw [isTree_iff, and_iff_right h.prop, isAcyclic_iff_forall_adj_isBridge]
  exact fun _ _ _ ↦
    by_contra fun hbr ↦
      h.not_prop_of_lt (by simpa [deleteEdges, ← edgeSet_ssubset_edgeSet]) <|
        h.prop.connected_delete_edge_of_not_isBridge hbr

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