SimpleGraph.IsTree.isConnected
theorem SimpleGraph.IsTree.isConnected : ∀ {V : Type u} {G : SimpleGraph V}, G.IsTree → G.Connected
This theorem asserts that for any given type `V` and any simple graph `G` of this type, if the graph `G` is a tree, then it is connected. In graph theory terms, a graph is said to be a tree if it is a undirected graph in which any two vertices are connected by exactly one path. The connectivity of a graph is guaranteed if it is a tree. This theorem essentially formalizes this property.
More concisely: If `G` is a simple undirected graph on type `V` such that `G` is a tree, then `G` is connected.
|
SimpleGraph.IsTree.IsAcyclic
theorem SimpleGraph.IsTree.IsAcyclic : ∀ {V : Type u} {G : SimpleGraph V}, G.IsTree → G.IsAcyclic
This theorem states that for any simple graph `G` with vertex type `V`, if `G` is a tree, then `G` is also acyclic. In other words, if a graph is a tree (a connected graph without any cycles), then it doesn't contain any cycles, hence it is acyclic. This theorem holds true for all types of vertices and all kinds of simple graphs.
More concisely: If a simple graph is a tree, then it is acyclic.
|