Properties of the ends of graphs

This file is meant to contain results about the ends of (locally finite connected) graphs.

instance SimpleGraph.instIsEmptyElemForallObjOppositeFinsetComponentComplFunctorEndOfFinite {V : Type} (G : SimpleGraph V) [Finite V] : IsEmpty ↑G.end

theorem SimpleGraph.end_componentCompl_infinite {V : Type} (G : SimpleGraph V) (e : ↑G.end) (K : (Finset V)ᵒᵖ) : (ComponentCompl.supp (↑e K)).Infinite

The componentCompls chosen by an end are all infinite.

instance SimpleGraph.componentComplFunctor_nonempty_of_infinite {V : Type} (G : SimpleGraph V) [Infinite V] (K : (Finset V)ᵒᵖ) : Nonempty (G.componentComplFunctor.obj K)

instance SimpleGraph.componentComplFunctor_finite {V : Type} (G : SimpleGraph V) [G.LocallyFinite] [Fact G.Preconnected] (K : (Finset V)ᵒᵖ) : Finite (G.componentComplFunctor.obj K)

theorem SimpleGraph.nonempty_ends_of_infinite {V : Type} (G : SimpleGraph V) [G.LocallyFinite] [Fact G.Preconnected] [Infinite V] : G.end.Nonempty

A locally finite preconnected infinite graph has at least one end.