# Documentation

Mathlib.Combinatorics.SimpleGraph.Ends.Defs

# Ends #

This file contains a definition of the ends of a simple graph, as sections of the inverse system assigning, to each finite set of vertices, the connected components of its complement.

@[reducible]
def SimpleGraph.ComponentCompl {V : Type u} (G : ) (K : Set V) :

The components outside a given set of vertices K

Instances For
@[reducible]
def SimpleGraph.componentComplMk {V : Type u} {K : Set V} (G : ) {v : V} (vK : ¬v K) :

The connected component of v in G.induce Kᶜ.

Instances For
def SimpleGraph.ComponentCompl.supp {V : Type u} {G : } {K : Set V} (C : ) :
Set V

The set of vertices of G making up the connected component C

Instances For
theorem SimpleGraph.ComponentCompl.supp_injective {V : Type u} {G : } {K : Set V} :
Function.Injective SimpleGraph.ComponentCompl.supp
theorem SimpleGraph.ComponentCompl.supp_inj {V : Type u} {G : } {K : Set V} {C : } {D : } :
instance SimpleGraph.ComponentCompl.setLike {V : Type u} {G : } {K : Set V} :
@[simp]
theorem SimpleGraph.ComponentCompl.mem_supp_iff {V : Type u} {G : } {K : Set V} {v : V} {C : } :
v C vK,
theorem SimpleGraph.componentComplMk_mem {V : Type u} {K : Set V} (G : ) {v : V} (vK : ¬v K) :
theorem SimpleGraph.componentComplMk_eq_of_adj {V : Type u} {K : Set V} (G : ) {v : V} {w : V} (vK : ¬v K) (wK : ¬w K) (a : ) :
instance SimpleGraph.componentCompl_nonempty_of_infinite {V : Type u} (G : ) [] (K : ) :

In an infinite graph, the set of components out of a finite set is nonempty.

def SimpleGraph.ComponentCompl.lift {V : Type u} {G : } {K : Set V} {β : Sort u_1} (f : v : V⦄ → ¬v Kβ) (h : ∀ ⦃v w : V⦄ (hv : ¬v K) (hw : ¬w K), f v hv = f w hw) :

A ComponentCompl specialization of Quot.lift, where soundness has to be proved only for adjacent vertices.

Instances For
theorem SimpleGraph.ComponentCompl.ind {V : Type u} {G : } {K : Set V} {β : } (f : v : V⦄ → (hv : ¬v K) → β ()) (C : ) :
β C
@[reducible]
def SimpleGraph.ComponentCompl.coeGraph {V : Type u} {G : } {K : Set V} (C : ) :
SimpleGraph { x // x C }

The induced graph on the vertices C.

Instances For
theorem SimpleGraph.ComponentCompl.coe_inj {V : Type u} {G : } {K : Set V} {C : } {D : } :
C = D C = D
@[simp]
theorem SimpleGraph.ComponentCompl.nonempty {V : Type u} {G : } {K : Set V} (C : ) :
theorem SimpleGraph.ComponentCompl.exists_eq_mk {V : Type u} {G : } {K : Set V} (C : ) :
v h,
theorem SimpleGraph.ComponentCompl.disjoint_right {V : Type u} {G : } {K : Set V} (C : ) :
Disjoint K C
theorem SimpleGraph.ComponentCompl.not_mem_of_mem {V : Type u} {G : } {K : Set V} {C : } {c : V} (cC : c C) :
¬c K
theorem SimpleGraph.ComponentCompl.pairwise_disjoint {V : Type u} {G : } {K : Set V} :
Pairwise fun C D => Disjoint C D
theorem SimpleGraph.ComponentCompl.mem_of_adj {V : Type u} {G : } {K : Set V} {C : } (c : V) (d : V) :
c C¬d Kd C

Any vertex adjacent to a vertex of C and not lying in K must lie in C.

theorem SimpleGraph.ComponentCompl.exists_adj_boundary_pair {V : Type u} {G : } {K : Set V} (Gc : ) (hK : ) (C : ) :
ck, ck.fst C ck.snd K SimpleGraph.Adj G ck.fst ck.snd

Assuming G is preconnected and K not empty, given any connected component C outside of K, there exists a vertex k ∈ K adjacent to a vertex v ∈ C.

@[reducible]
def SimpleGraph.ComponentCompl.hom {V : Type u} {G : } {K : Set V} {L : Set V} (h : K L) (C : ) :

If K ⊆ L, the components outside of L are all contained in a single component outside of K.

Instances For
theorem SimpleGraph.ComponentCompl.subset_hom {V : Type u} {G : } {K : Set V} {L : Set V} (C : ) (h : K L) :
C
theorem SimpleGraph.componentComplMk_mem_hom {V : Type u} {K : Set V} {L : Set V} (G : ) {v : V} (vK : ¬v K) (h : L K) :
theorem SimpleGraph.ComponentCompl.hom_eq_iff_le {V : Type u} {G : } {K : Set V} {L : Set V} (C : ) (h : K L) (D : ) :
C D
theorem SimpleGraph.ComponentCompl.hom_eq_iff_not_disjoint {V : Type u} {G : } {K : Set V} {L : Set V} (C : ) (h : K L) (D : ) :
¬Disjoint C D
theorem SimpleGraph.ComponentCompl.hom_refl {V : Type u} {G : } {L : Set V} (C : ) :
theorem SimpleGraph.ComponentCompl.hom_trans {V : Type u} {G : } {K : Set V} {L : Set V} {M : Set V} (C : ) (h : K L) (h' : M K) :
theorem SimpleGraph.ComponentCompl.hom_mk {V : Type u} {G : } {K : Set V} {L : Set V} {v : V} (vnL : ¬v L) (h : K L) :
theorem SimpleGraph.ComponentCompl.hom_infinite {V : Type u} {G : } {K : Set V} {L : Set V} (C : ) (h : K L) (Cinf : ) :
theorem SimpleGraph.ComponentCompl.infinite_iff_in_all_ranges {V : Type u} {G : } {K : } (C : ) :
∀ (L : ) (h : K L), D,
instance SimpleGraph.componentCompl_finite {V : Type u} {G : } [Gpc : ] (K : ) :
@[simp]
theorem SimpleGraph.componentComplFunctor_obj {V : Type u} (G : ) (K : ()ᵒᵖ) :
().obj K = SimpleGraph.ComponentCompl G K.unop
@[simp]
theorem SimpleGraph.componentComplFunctor_map {V : Type u} (G : ) :
∀ {X Y : ()ᵒᵖ} (f : X Y) (C : SimpleGraph.ComponentCompl G X.unop), ().map f C = SimpleGraph.ComponentCompl.hom (_ : Y.unop X.unop) C

The functor assigning, to a finite set in V, the set of connected components in its complement.

Instances For
def SimpleGraph.end {V : Type u} (G : ) :
Set ((j : ()ᵒᵖ) → ().obj j)

The end of a graph, defined as the sections of the functor component_compl_functor .

Instances For
theorem SimpleGraph.end_hom_mk_of_mk {V : Type u} (G : ) {s : (j : ()ᵒᵖ) → ().obj j} (sec : ) {K : ()ᵒᵖ} {L : ()ᵒᵖ} (h : L K) {v : V} (vnL : ¬v L.unop) (hs : s L = ) :
s K = SimpleGraph.componentComplMk G (_ : ¬v fun a => a K.unop.val)
theorem SimpleGraph.infinite_iff_in_eventualRange {V : Type u} (G : ) {K : ()ᵒᵖ} (C : ().obj K) :