Representation of components by a set of vertices

Main definition

• SimpleGraph.ConnectedComponent.Represents says that a set of vertices represents a set of components if it contains exactly one vertex from each component.

def SimpleGraph.ConnectedComponent.Represents {V : Type u} {G : SimpleGraph V} (s : Set V) (C : Set G.ConnectedComponent) : Prop

A set of vertices represents a set of components if it contains exactly one vertex from each component.

theorem SimpleGraph.ConnectedComponent.Represents.image_out {V : Type u} {G : SimpleGraph V} (C : Set G.ConnectedComponent) : Represents (Quot.out '' C) C

theorem SimpleGraph.ConnectedComponent.Represents.existsUnique_rep {V : Type u} {G : SimpleGraph V} {C : Set G.ConnectedComponent} {s : Set V} {c : G.ConnectedComponent} (hrep : Represents s C) (h : c ∈ C) : ∃! x : V, x ∈ s ∩ c.supp

theorem SimpleGraph.ConnectedComponent.Represents.exists_inter_eq_singleton {V : Type u} {G : SimpleGraph V} {C : Set G.ConnectedComponent} {s : Set V} {c : G.ConnectedComponent} (hrep : Represents s C) (h : c ∈ C) : ∃ (x : V), s ∩ c.supp = {x}

theorem SimpleGraph.ConnectedComponent.Represents.disjoint_supp_of_notMem {V : Type u} {G : SimpleGraph V} {C : Set G.ConnectedComponent} {s : Set V} {c : G.ConnectedComponent} (hrep : Represents s C) (h : c ∉ C) : Disjoint s c.supp

theorem SimpleGraph.ConnectedComponent.Represents.ncard_inter {V : Type u} {G : SimpleGraph V} {C : Set G.ConnectedComponent} {s : Set V} {c : G.ConnectedComponent} (hrep : Represents s C) (h : c ∈ C) : (s ∩ c.supp).ncard = 1

theorem SimpleGraph.ConnectedComponent.Represents.ncard_eq {V : Type u} {G : SimpleGraph V} {C : Set G.ConnectedComponent} {s : Set V} (hrep : Represents s C) : s.ncard = C.ncard

theorem SimpleGraph.ConnectedComponent.Represents.ncard_sdiff_of_mem {V : Type u} {G : SimpleGraph V} {C : Set G.ConnectedComponent} {s : Set V} {c : G.ConnectedComponent} (hrep : Represents s C) (h : c ∈ C) : (c.supp \ s).ncard = c.supp.ncard - 1

theorem SimpleGraph.ConnectedComponent.Represents.ncard_sdiff_of_notMem {V : Type u} {G : SimpleGraph V} {C : Set G.ConnectedComponent} {s : Set V} {c : G.ConnectedComponent} (hrep : Represents s C) (h : c ∉ C) : (c.supp \ s).ncard = c.supp.ncard

theorem SimpleGraph.ConnectedComponent.even_ncard_supp_sdiff_rep {V : Type u} {G : SimpleGraph V} {s : Set V} (K : G.ConnectedComponent) (hrep : Represents s G.oddComponents) : Even (K.supp \ s).ncard