theorem SimpleGraph.edgeSet_finite_of_support_finite {V : Type} {graph : SimpleGraph V} (hfin : graph.support.Finite) : graph.edgeSet.Finite

If the support of a simple graph is finite, then so is its edge set.

theorem SimpleGraph.exist_edge_end_walk {V : Type} {graph : SimpleGraph V} {v u : V} (h1 : v ≠ u) (walk : graph.Walk v u) : ∃ e ∈ graph.edgeSet, u ∈ e

If a non-empty walk ends with a vertex u, then there exists some edge incident to u.