Documentation

Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Connectivity of subgraphs and induced graphs #

Main definitions #

A subgraph is preconnected if it is preconnected when coerced to be a simple graph.

Note: This is a structure to make it so one can be precise about how dot notation resolves.

Instances For

    A subgraph is connected if it is connected when coerced to be a simple graph.

    Note: This is a structure to make it so one can be precise about how dot notation resolves.

    Instances For
      theorem SimpleGraph.induce_connected_adj_union {V : Type u} {G : SimpleGraph V} {v : V} {w : V} {s : Set V} {t : Set V} (sconn : SimpleGraph.Connected (SimpleGraph.induce s G)) (tconn : SimpleGraph.Connected (SimpleGraph.induce t G)) (hv : v s) (hw : w t) (ha : SimpleGraph.Adj G v w) :
      theorem SimpleGraph.induce_connected_of_patches {V : Type u} {G : SimpleGraph V} {s : Set V} (u : V) (hu : u s) (patches : ∀ {v : V}, v ss' x hu' hv', SimpleGraph.Reachable (SimpleGraph.induce s' G) { val := u, property := hu' } { val := v, property := hv' }) :
      theorem SimpleGraph.induce_sUnion_connected_of_pairwise_not_disjoint {V : Type u} {G : SimpleGraph V} {S : Set (Set V)} (Sn : Set.Nonempty S) (Snd : ∀ {s t : Set V}, s St SSet.Nonempty (s t)) (Sc : ∀ {s : Set V}, s SSimpleGraph.Connected (SimpleGraph.induce s G)) :