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.

source
@[reducible]
def simple_graph.component_compl {V : Type u} (G : simple_graph V) (K : set V) :
Type u

The components outside a given set of vertices K

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

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

Equations
source
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
source
@[ext]
theorem simple_graph.component_compl.supp_injective {V : Type u} {G : simple_graph V} {K : set V} :
function.injective simple_graph.component_compl.supp
source
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
source
@[protected, instance]
def simple_graph.component_compl.set_like {V : Type u} {G : simple_graph V} {K : set V} :
set_like (G.component_compl K) V
Equations
source
@[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
source
theorem simple_graph.component_compl_mk_mem {V : Type u} {K : set V} (G : simple_graph V) {v : V} (vK : v ∉ K) :
v ∈ G.component_compl_mk vK
source
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) :
G.component_compl_mk vK = G.component_compl_mk wK
source
@[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) :
G.component_compl K → β

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

Equations
source
@[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
source
@[protected, reducible]
def simple_graph.component_compl.coe_graph {V : Type u} {G : simple_graph V} {K : set V} (C : G.component_compl K) :
simple_graph ↥C

The induced graph on the vertices C.

Equations
source
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
source
@[protected, simp]
theorem simple_graph.component_compl.nonempty {V : Type u} {G : simple_graph V} {K : set V} (C : G.component_compl K) :
↑C.nonempty
source
@[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
source
@[protected]
theorem simple_graph.component_compl.disjoint_right {V : Type u} {G : simple_graph V} {K : set V} (C : G.component_compl K) :
disjoint K ↑C
source
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
source
@[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), disjoint ↑C ↑D)
source
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.

source
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.

source
@[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) :
G.component_compl K

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

Equations
source
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) :
↑C ⊆ ↑(simple_graph.component_compl.hom h C)
source
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) :
v ∈ simple_graph.component_compl.hom h (G.component_compl_mk vK)
source
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) :
simple_graph.component_compl.hom h C = D ↔ ↑C ⊆ ↑D
source
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) :
simple_graph.component_compl.hom h C = D ↔ ¬disjoint ↑C ↑D
source
theorem simple_graph.component_compl.hom_refl {V : Type u} {G : simple_graph V} {L : set V} (C : G.component_compl L) :
simple_graph.component_compl.hom _ C = C
source
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) :
simple_graph.component_compl.hom _ C = simple_graph.component_compl.hom h' (simple_graph.component_compl.hom h C)
source
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) :
simple_graph.component_compl.hom h (G.component_compl_mk vnL) = G.component_compl_mk _
source
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) :
↑(simple_graph.component_compl.hom h C).infinite
source
theorem simple_graph.component_compl.infinite_iff_in_all_ranges {V : Type u} {G : simple_graph V} {K : finset V} (C : G.component_compl ↑K) :
C.supp.infinite ↔ ∀ (L : finset V) (h : K ⊆ L), ∃ (D : G.component_compl ↑L), simple_graph.component_compl.hom h D = C
source
@[simp]
theorem simple_graph.component_compl_functor_obj {V : Type u} (G : simple_graph V) (K : (finset V)ᵒᵖ) :
G.component_compl_functor.obj K = G.component_compl ↑(opposite.unop K)
source
@[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)) :
G.component_compl_functor.map f C = simple_graph.component_compl.hom _ C
source
def simple_graph.component_compl_functor {V : Type u} (G : simple_graph V) :
(finset V)ᵒᵖ ⥤ Type u

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

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

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

Equations
Instances for ↥simple_graph.end
source
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) :
s K = G.component_compl_mk _
source
theorem simple_graph.infinite_iff_in_eventual_range {V : Type u} (G : simple_graph V) {K : (finset V)ᵒᵖ} (C : G.component_compl_functor.obj K) :
(simple_graph.component_compl.supp C).infinite ↔ C ∈ G.component_compl_functor.eventual_range K