Gluing induced graph pieces along a retained clique

Both pieces are induced subgraphs of one graph, cover its vertices and have no edges between their exclusive parts. Every edge of the shared clique is retained. This is not the convention of clique sums allowing separator-edge deletion. Edge accounting does not imply additivity of packing optima.

structure SimpleGraph.CliqueGluing {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (A B : Finset V) : Prop

A graph is the union of two induced pieces with a retained clique overlap.

• cover : A ∪ B = Finset.univ

  The two pieces cover every vertex.

• overlap_isClique : G.IsClique ↑(A ∩ B)

  The shared vertices form a clique in the original graph.

• no_cross (u : V) : u ∈ A → u ∉ B → ∀ v ∈ B, v ∉ A → ¬G.Adj u v

  No edge joins the two exclusive parts.

theorem SimpleGraph.CliqueGluing.mem_left_or_right {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} {A B : Finset V} (h : G.CliqueGluing A B) (v : V) : v ∈ A ∨ v ∈ B

Every vertex belongs to at least one piece.

theorem SimpleGraph.CliqueGluing.neighbor_mem_left {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} {A B : Finset V} (h : G.CliqueGluing A B) {u v : V} (hu : u ∈ A) (huB : u ∉ B) (huv : G.Adj u v) : v ∈ A

All neighbours of a vertex exclusive to the left piece stay in that piece.

theorem SimpleGraph.CliqueGluing.edge_in_piece {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} {A B : Finset V} (h : G.CliqueGluing A B) {u v : V} (huv : G.Adj u v) : u ∈ A ∧ v ∈ A ∨ u ∈ B ∧ v ∈ B

Every edge is entirely contained in one of the induced pieces.

theorem SimpleGraph.CliqueGluing.card_vertices_add_overlap {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} {A B : Finset V} (h : G.CliqueGluing A B) : Fintype.card V + (A ∩ B).card = A.card + B.card

Vertex accounting counts the overlap only once.