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 : SimpleGraph V) (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 : SimpleGraph V) {v : V} (vK : ¬v K) :

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

    Instances For

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

      Instances For
        theorem SimpleGraph.ComponentCompl.supp_injective {V : Type u} {G : SimpleGraph V} {K : Set V} :
        Function.Injective SimpleGraph.ComponentCompl.supp
        @[simp]
        theorem SimpleGraph.componentComplMk_mem {V : Type u} {K : Set V} (G : SimpleGraph V) {v : V} (vK : ¬v K) :
        theorem SimpleGraph.componentComplMk_eq_of_adj {V : Type u} {K : Set V} (G : SimpleGraph V) {v : V} {w : V} (vK : ¬v K) (wK : ¬w K) (a : SimpleGraph.Adj G v w) :

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

        def SimpleGraph.ComponentCompl.lift {V : Type u} {G : SimpleGraph V} {K : Set V} {β : Sort u_1} (f : v : V⦄ → ¬v Kβ) (h : ∀ ⦃v w : V⦄ (hv : ¬v K) (hw : ¬w K), SimpleGraph.Adj G v wf 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 : SimpleGraph V} {K : Set V} {β : SimpleGraph.ComponentCompl G KProp} (f : v : V⦄ → (hv : ¬v K) → β (SimpleGraph.componentComplMk G hv)) (C : SimpleGraph.ComponentCompl G K) :
          β C
          @[reducible]

          The induced graph on the vertices C.

          Instances For
            theorem SimpleGraph.ComponentCompl.not_mem_of_mem {V : Type u} {G : SimpleGraph V} {K : Set V} {C : SimpleGraph.ComponentCompl G K} {c : V} (cC : c C) :
            ¬c K
            theorem SimpleGraph.ComponentCompl.pairwise_disjoint {V : Type u} {G : SimpleGraph V} {K : Set V} :
            Pairwise fun C D => Disjoint C D
            theorem SimpleGraph.ComponentCompl.mem_of_adj {V : Type u} {G : SimpleGraph V} {K : Set V} {C : SimpleGraph.ComponentCompl G K} (c : V) (d : V) :
            c C¬d KSimpleGraph.Adj G c dd 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 : SimpleGraph V} {K : Set V} (Gc : SimpleGraph.Preconnected G) (hK : Set.Nonempty K) (C : SimpleGraph.ComponentCompl G K) :
            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]

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

            Instances For
              theorem SimpleGraph.componentComplMk_mem_hom {V : Type u} {K : Set V} {L : Set V} (G : SimpleGraph V) {v : V} (vK : ¬v K) (h : L K) :
              @[simp]
              theorem SimpleGraph.componentComplFunctor_map {V : Type u} (G : SimpleGraph V) :
              ∀ {X Y : (Finset V)ᵒᵖ} (f : X Y) (C : SimpleGraph.ComponentCompl G X.unop), (SimpleGraph.componentComplFunctor G).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 : SimpleGraph V) :

                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 : SimpleGraph V) {s : (j : (Finset V)ᵒᵖ) → (SimpleGraph.componentComplFunctor G).obj j} (sec : s SimpleGraph.end G) {K : (Finset V)ᵒᵖ} {L : (Finset V)ᵒᵖ} (h : L K) {v : V} (vnL : ¬v L.unop) (hs : s L = SimpleGraph.componentComplMk G vnL) :
                  s K = SimpleGraph.componentComplMk G (_ : ¬v fun a => a K.unop.val)