Exact edge accounting for clique gluing

All counts use Mathlib's induced graphs and literal edge finsets. The edges in the overlap are counted twice by the pieces and once by the whole graph.

theorem SimpleGraph.CliqueGluing.union_piece_edges {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {A B : Finset V} (h : G.CliqueGluing A B) : {e ∈ G.edgeFinset | e.toFinset ⊆ A} ∪ {e ∈ G.edgeFinset | e.toFinset ⊆ B} = G.edgeFinset

The ambient edge sets of the two induced pieces cover the graph edges.

theorem SimpleGraph.CliqueGluing.inter_piece_edges {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {A B : Finset V} : {e ∈ G.edgeFinset | e.toFinset ⊆ A} ∩ {e ∈ G.edgeFinset | e.toFinset ⊆ B} = {e ∈ G.edgeFinset | e.toFinset ⊆ A ∩ B}

The common edges are exactly those induced by the overlap.

theorem SimpleGraph.CliqueGluing.card_edges_add_overlap {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {A B : Finset V} (h : G.CliqueGluing A B) : G.edgeFinset.card + (induce (↑(A ∩ B)) G).edgeFinset.card = (induce (↑A) G).edgeFinset.card + (induce (↑B) G).edgeFinset.card

Edge accounting in terms of the three literal induced subgraphs.

theorem SimpleGraph.CliqueGluing.card_overlap_edges {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {A B : Finset V} (h : G.CliqueGluing A B) : (induce (↑(A ∩ B)) G).edgeFinset.card = (A ∩ B).card.choose 2

A retained clique overlap has exactly one edge per pair of distinct vertices.

theorem SimpleGraph.CliqueGluing.card_edges_add_choose_overlap {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {A B : Finset V} (h : G.CliqueGluing A B) : G.edgeFinset.card + (A ∩ B).card.choose 2 = (induce (↑A) G).edgeFinset.card + (induce (↑B) G).edgeFinset.card

The clique-overlap form of inclusion-exclusion for graph edges.