SimpleGraph.end_componentCompl_infinite
theorem SimpleGraph.end_componentCompl_infinite :
∀ {V : Type} (G : SimpleGraph V) (e : ↑G.end) (K : (Finset V)ᵒᵖ),
(SimpleGraph.ComponentCompl.supp (↑e K)).Infinite
The theorem `SimpleGraph.end_componentCompl_infinite` states that for any type `V`, any simple graph `G` of type `V`, any end `e` of `G`, and any set `K` of vertices, the set of vertices that make up the complement component chosen by end `e` (`SimpleGraph.ComponentCompl.supp (↑e K)`) is infinite. In other words, the theorem asserts that all complement components chosen by an end in a simple graph are infinite.
More concisely: For any simple graph and any end, the complement component chosen by that end is infinite.
|
SimpleGraph.nonempty_ends_of_infinite
theorem SimpleGraph.nonempty_ends_of_infinite :
∀ {V : Type} (G : SimpleGraph V) [inst : G.LocallyFinite] [inst : Fact G.Preconnected] [inst : Infinite V],
G.end.Nonempty
The theorem states that for any infinite, preconnected and locally finite simple graph, there always exists at least one end. Here, a simple graph is defined over a set `V` and is locally finite if at every vertex `v` in `V` there is a neighborhood of `v` which meets only finitely many other vertices in the graph. The graph is preconnected if there is a path between any two vertices. An end of a graph is intuitively a "direction" in which the graph extends to infinity. According to the theorem, such an end always exists in the graph under the given conditions.
More concisely: Every infinite, locally finite, preconnected simple graph has at least one end.
|