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, inline]
abbrev SimpleGraph.ComponentCompl {V : Type u} (G : SimpleGraph V) (K : Set V) :

The components outside a given set of vertices K

Equations
Instances For
    @[reducible, inline]
    abbrev SimpleGraph.componentComplMk {V : Type u} {K : Set V} (G : SimpleGraph V) {v : V} (vK : vK) :
    G.ComponentCompl K

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

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

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

      Equations
      • C.supp = {v : V | ∃ (h : vK), G.componentComplMk h = C}
      Instances For
        theorem SimpleGraph.ComponentCompl.supp_injective {V : Type u} {G : SimpleGraph V} {K : Set V} :
        Function.Injective SimpleGraph.ComponentCompl.supp
        theorem SimpleGraph.ComponentCompl.supp_inj {V : Type u} {G : SimpleGraph V} {K : Set V} {C : G.ComponentCompl K} {D : G.ComponentCompl K} :
        C.supp = D.supp C = D
        instance SimpleGraph.ComponentCompl.setLike {V : Type u} {G : SimpleGraph V} {K : Set V} :
        SetLike (G.ComponentCompl K) V
        Equations
        • SimpleGraph.ComponentCompl.setLike = { coe := SimpleGraph.ComponentCompl.supp, coe_injective' := }
        @[simp]
        theorem SimpleGraph.ComponentCompl.mem_supp_iff {V : Type u} {G : SimpleGraph V} {K : Set V} {v : V} {C : G.ComponentCompl K} :
        v C ∃ (vK : vK), G.componentComplMk vK = C
        theorem SimpleGraph.componentComplMk_mem {V : Type u} {K : Set V} (G : SimpleGraph V) {v : V} (vK : vK) :
        v G.componentComplMk vK
        theorem SimpleGraph.componentComplMk_eq_of_adj {V : Type u} {K : Set V} (G : SimpleGraph V) {v : V} {w : V} (vK : vK) (wK : wK) (a : G.Adj v w) :
        G.componentComplMk vK = G.componentComplMk wK
        instance SimpleGraph.componentCompl_nonempty_of_infinite {V : Type u} (G : SimpleGraph V) [Infinite V] (K : Finset V) :
        Nonempty (G.ComponentCompl K)

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

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

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

        Equations
        Instances For
          theorem SimpleGraph.ComponentCompl.ind {V : Type u} {G : SimpleGraph V} {K : Set V} {β : G.ComponentCompl KProp} (f : ∀ ⦃v : V⦄ (hv : vK), β (G.componentComplMk hv)) (C : G.ComponentCompl K) :
          β C
          @[reducible, inline]
          abbrev SimpleGraph.ComponentCompl.coeGraph {V : Type u} {G : SimpleGraph V} {K : Set V} (C : G.ComponentCompl K) :

          The induced graph on the vertices C.

          Equations
          Instances For
            theorem SimpleGraph.ComponentCompl.coe_inj {V : Type u} {G : SimpleGraph V} {K : Set V} {C : G.ComponentCompl K} {D : G.ComponentCompl K} :
            C = D C = D
            @[simp]
            theorem SimpleGraph.ComponentCompl.nonempty {V : Type u} {G : SimpleGraph V} {K : Set V} (C : G.ComponentCompl K) :
            (C).Nonempty
            theorem SimpleGraph.ComponentCompl.exists_eq_mk {V : Type u} {G : SimpleGraph V} {K : Set V} (C : G.ComponentCompl K) :
            ∃ (v : V) (h : vK), G.componentComplMk h = C
            theorem SimpleGraph.ComponentCompl.disjoint_right {V : Type u} {G : SimpleGraph V} {K : Set V} (C : G.ComponentCompl K) :
            Disjoint K C
            theorem SimpleGraph.ComponentCompl.not_mem_of_mem {V : Type u} {G : SimpleGraph V} {K : Set V} {C : G.ComponentCompl K} {c : V} (cC : c C) :
            cK
            theorem SimpleGraph.ComponentCompl.pairwise_disjoint {V : Type u} {G : SimpleGraph V} {K : Set V} :
            Pairwise fun (C D : G.ComponentCompl K) => Disjoint C D
            theorem SimpleGraph.ComponentCompl.mem_of_adj {V : Type u} {G : SimpleGraph V} {K : Set V} {C : G.ComponentCompl K} (c : V) (d : V) :
            c CdKG.Adj 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 : G.Preconnected) (hK : K.Nonempty) (C : G.ComponentCompl K) :
            ∃ (ck : V × V), ck.1 C ck.2 K G.Adj ck.1 ck.2

            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, inline]
            abbrev SimpleGraph.ComponentCompl.hom {V : Type u} {G : SimpleGraph V} {K : Set V} {L : Set V} (h : K L) (C : G.ComponentCompl L) :
            G.ComponentCompl K

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

            Equations
            Instances For
              theorem SimpleGraph.ComponentCompl.subset_hom {V : Type u} {G : SimpleGraph V} {K : Set V} {L : Set V} (C : G.ComponentCompl L) (h : K L) :
              theorem SimpleGraph.componentComplMk_mem_hom {V : Type u} {K : Set V} {L : Set V} (G : SimpleGraph V) {v : V} (vK : vK) (h : L K) :
              v SimpleGraph.ComponentCompl.hom h (G.componentComplMk vK)
              theorem SimpleGraph.ComponentCompl.hom_eq_iff_le {V : Type u} {G : SimpleGraph V} {K : Set V} {L : Set V} (C : G.ComponentCompl L) (h : K L) (D : G.ComponentCompl K) :
              theorem SimpleGraph.ComponentCompl.hom_eq_iff_not_disjoint {V : Type u} {G : SimpleGraph V} {K : Set V} {L : Set V} (C : G.ComponentCompl L) (h : K L) (D : G.ComponentCompl K) :
              theorem SimpleGraph.ComponentCompl.hom_refl {V : Type u} {G : SimpleGraph V} {L : Set V} (C : G.ComponentCompl L) :
              theorem SimpleGraph.ComponentCompl.hom_trans {V : Type u} {G : SimpleGraph V} {K : Set V} {L : Set V} {M : Set V} (C : G.ComponentCompl L) (h : K L) (h' : M K) :
              theorem SimpleGraph.ComponentCompl.hom_mk {V : Type u} {G : SimpleGraph V} {K : Set V} {L : Set V} {v : V} (vnL : vL) (h : K L) :
              SimpleGraph.ComponentCompl.hom h (G.componentComplMk vnL) = G.componentComplMk
              theorem SimpleGraph.ComponentCompl.hom_infinite {V : Type u} {G : SimpleGraph V} {K : Set V} {L : Set V} (C : G.ComponentCompl L) (h : K L) (Cinf : (C).Infinite) :
              ((SimpleGraph.ComponentCompl.hom h C)).Infinite
              theorem SimpleGraph.ComponentCompl.infinite_iff_in_all_ranges {V : Type u} {G : SimpleGraph V} {K : Finset V} (C : G.ComponentCompl K) :
              C.supp.Infinite ∀ (L : Finset V) (h : K L), ∃ (D : G.ComponentCompl L), SimpleGraph.ComponentCompl.hom h D = C
              instance SimpleGraph.componentCompl_finite {V : Type u} {G : SimpleGraph V} [G.LocallyFinite] [Gpc : Fact G.Preconnected] (K : Finset V) :
              Finite (G.ComponentCompl K)

              For a locally finite preconnected graph, the number of components outside of any finite set is finite.

              Equations
              • =
              @[simp]
              theorem SimpleGraph.componentComplFunctor_obj {V : Type u} (G : SimpleGraph V) (K : (Finset V)ᵒᵖ) :
              G.componentComplFunctor.obj K = G.ComponentCompl (Opposite.unop K)
              @[simp]
              theorem SimpleGraph.componentComplFunctor_map {V : Type u} (G : SimpleGraph V) :
              ∀ {X Y : (Finset V)ᵒᵖ} (f : X Y) (C : G.ComponentCompl (Opposite.unop X)), G.componentComplFunctor.map f C = SimpleGraph.ComponentCompl.hom C

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

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                def SimpleGraph.end {V : Type u} (G : SimpleGraph V) :
                Set ((j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j)

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

                Equations
                • G.end = G.componentComplFunctor.sections
                Instances For
                  theorem SimpleGraph.end_hom_mk_of_mk {V : Type u} (G : SimpleGraph V) {s : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j} (sec : s G.end) {K : (Finset V)ᵒᵖ} {L : (Finset V)ᵒᵖ} (h : L K) {v : V} (vnL : vOpposite.unop L) (hs : s L = G.componentComplMk vnL) :
                  s K = G.componentComplMk
                  theorem SimpleGraph.infinite_iff_in_eventualRange {V : Type u} (G : SimpleGraph V) {K : (Finset V)ᵒᵖ} (C : G.componentComplFunctor.obj K) :
                  (SimpleGraph.ComponentCompl.supp C).Infinite C G.componentComplFunctor.eventualRange K