Properties of the ends of graphs

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

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

Equations

• (_ : IsEmpty ↑(SimpleGraph.end G)) = (_ : IsEmpty ↑(SimpleGraph.end G))

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

The componentCompls chosen by an end are all infinite.

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

Equations

• (_ : Nonempty ((SimpleGraph.componentComplFunctor G).toPrefunctor.obj K)) = (_ : Nonempty (SimpleGraph.ComponentCompl G ↑K.unop))

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

Equations

• (_ : Finite ((SimpleGraph.componentComplFunctor G).toPrefunctor.obj K)) = (_ : Finite (SimpleGraph.ComponentCompl G ↑K.unop))

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

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