mathlib3documentation

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
@[ext]
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
@[protected, instance]
Equations
@[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), = C
theorem simple_graph.component_compl_mk_mem {V : Type u} {K : set V} (G : simple_graph V) {v : V} (vK : v K) :
v
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} {β : 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]
theorem simple_graph.component_compl.nonempty {V : Type u} {G : simple_graph V} {K : set V} (C : G.component_compl K) :
@[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), = 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.pairwise_disjoint {V : Type u} {G : simple_graph V} {K : set V} :
pairwise (λ (C D : G.component_compl K), D)
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.subset_hom {V : Type u} {G : simple_graph V} {K L : set V} (C : G.component_compl L) (h : K L) :
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_eq_iff_le {V : Type u} {G : simple_graph V} {K L : set V} (C : G.component_compl L) (h : K L) (D : G.component_compl K) :
theorem simple_graph.component_compl.hom_eq_iff_not_disjoint {V : Type u} {G : simple_graph V} {K L : set V} (C : G.component_compl L) (h : K L) (D : G.component_compl K) :
theorem simple_graph.component_compl.hom_refl {V : Type u} {G : simple_graph V} {L : set V} (C : G.component_compl L) :
theorem simple_graph.component_compl.hom_trans {V : Type u} {G : simple_graph V} {K L M : set V} (C : G.component_compl L) (h : K L) (h' : M 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) :
theorem simple_graph.component_compl.hom_infinite {V : Type u} {G : simple_graph V} {K L : set V} (C : G.component_compl L) (h : K L) (Cinf : C.infinite) :
@[simp]
@[simp]
theorem simple_graph.component_compl_functor_map {V : Type u} (G : simple_graph V) (_x _x_1 : (finset V)ᵒᵖ) (f : _x _x_1) (C : G.component_compl (opposite.unop _x)) :

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

Equations
@[protected]
def simple_graph.end {V : Type u} (G : simple_graph V) :
set (Π (j : (finset V)ᵒᵖ),

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)ᵒᵖ), } (sec : s G.end) {K L : (finset V)ᵒᵖ} (h : L K) {v : V} (vnL : v ) (hs : s L = G.component_compl_mk vnL) :
s K =