mathlib3 documentation

combinatorics.simple_graph.ends.defs

Ends #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 simple_graph.component_compl {V : Type u} (G : simple_graph V) (K : set V) :

The components outside a given set of vertices K

Equations
@[reducible]
def simple_graph.component_compl_mk {V : Type u} {K : set V} (G : simple_graph V) {v : V} (vK : v K) :

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

Equations
def simple_graph.component_compl.supp {V : Type u} {G : simple_graph V} {K : set V} (C : G.component_compl K) :
set V

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

Equations
theorem simple_graph.component_compl.supp_inj {V : Type u} {G : simple_graph V} {K : set V} {C D : G.component_compl K} :
C.supp = D.supp C = D
@[simp]
theorem simple_graph.component_compl.mem_supp_iff {V : Type u} {G : simple_graph V} {K : set V} {v : V} {C : G.component_compl K} :
v C (vK : v K), G.component_compl_mk vK = C
theorem simple_graph.component_compl_mk_mem {V : Type u} {K : set V} (G : simple_graph V) {v : V} (vK : v K) :
theorem simple_graph.component_compl_mk_eq_of_adj {V : Type u} {K : set V} (G : simple_graph V) {v w : V} (vK : v K) (wK : w K) (a : G.adj v w) :
@[protected]
def simple_graph.component_compl.lift {V : Type u} {G : simple_graph V} {K : set V} {β : Sort u_1} (f : Π ⦃v : V⦄, v K β) (h : ⦃v w : V⦄ (hv : v K) (hw : w K), G.adj v w f hv = f hw) :

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

Equations
@[protected]
theorem simple_graph.component_compl.ind {V : Type u} {G : simple_graph V} {K : set V} {β : G.component_compl K Prop} (f : ⦃v : V⦄ (hv : v K), β (G.component_compl_mk hv)) (C : G.component_compl K) :
β C
@[protected, reducible]

The induced graph on the vertices C.

Equations
theorem simple_graph.component_compl.coe_inj {V : Type u} {G : simple_graph V} {K : set V} {C D : G.component_compl K} :
C = D C = D
@[protected, simp]
@[protected]
theorem simple_graph.component_compl.exists_eq_mk {V : Type u} {G : simple_graph V} {K : set V} (C : G.component_compl K) :
(v : V) (h : v K), G.component_compl_mk h = C
@[protected]
theorem simple_graph.component_compl.not_mem_of_mem {V : Type u} {G : simple_graph V} {K : set V} {C : G.component_compl K} {c : V} (cC : c C) :
c K
@[protected]
theorem simple_graph.component_compl.mem_of_adj {V : Type u} {G : simple_graph V} {K : set V} {C : G.component_compl K} (c d : V) :
c C d K G.adj c d d C

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

theorem simple_graph.component_compl.exists_adj_boundary_pair {V : Type u} {G : simple_graph V} {K : set V} (Gc : G.preconnected) (hK : K.nonempty) (C : G.component_compl K) :
(ck : V × V), ck.fst C ck.snd K G.adj 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 simple_graph.component_compl.hom {V : Type u} {G : simple_graph V} {K L : set V} (h : K L) (C : G.component_compl L) :

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

Equations
theorem simple_graph.component_compl_mk_mem_hom {V : Type u} {K L : set V} (G : simple_graph V) {v : V} (vK : v K) (h : L K) :
theorem simple_graph.component_compl.hom_mk {V : Type u} {G : simple_graph V} {K L : set V} {v : V} (vnL : v L) (h : K L) :

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

Equations
@[protected]

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

Equations
Instances for simple_graph.end
theorem simple_graph.end_hom_mk_of_mk {V : Type u} (G : simple_graph V) {s : Π (j : (finset V)ᵒᵖ), G.component_compl_functor.obj j} (sec : s G.end) {K L : (finset V)ᵒᵖ} (h : L K) {v : V} (vnL : v opposite.unop L) (hs : s L = G.component_compl_mk vnL) :