isTree_connectedComponent — Mathlib

English

A connected component of an acyclic graph is a tree.

Русский

Связанная компонента ацикличного графа является деревом.

LaTeX

$$$G.IsAcyclic \Rightarrow \forall c: G.ConnectedComponent, c.toSimpleGraph.IsTree$$$

Lean4

/-- A connected component of an acyclic graph is a tree. -/
theorem isTree_connectedComponent (h : G.IsAcyclic) (c : G.ConnectedComponent) : c.toSimpleGraph.IsTree
    where
  isConnected := c.connected_toSimpleGraph
  IsAcyclic := h.comap c.toSimpleGraph_hom <| by simp [ConnectedComponent.toSimpleGraph_hom]

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