Edge Count via Kelly's Lemma #
Edge count is a special case of Kelly's Lemma: the number of induced copies
of K₂ (the complete graph on 2 vertices) in G equals |E(G)|.
This connects the ad-hoc edge count proof in EdgeCount.lean to the general
subgraph counting framework in KellyLemma.lean.
Main results #
SimpleGraph.subgraphCount_completeGraph_two—s(K₂, G) = |E(G)|SimpleGraph.SameDeck.card_edgeFinset_eq'— edge count reconstructibility via Kelly's Lemma
theorem
SimpleGraph.subgraphCount_completeGraph_two
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
:
The number of induced copies of K₂ in G equals the number of edges of G.
A 2-element subset S ⊆ V satisfies G[S] ≅ K₂ if and only if the two
vertices in S are adjacent in G.
theorem
SimpleGraph.SameDeck.card_edgeFinset_eq'
{V : Type u_1}
[Fintype V]
[DecidableEq V]
{G H : SimpleGraph V}
(h : G.SameDeck H)
(hV : 3 ≤ Fintype.card V)
:
Edge count is reconstructible (via Kelly's Lemma). If |V| ≥ 3 and two
graphs have the same deck, they have the same number of edges.
This is a direct corollary: |E(G)| = s(K₂, G), and Kelly's Lemma gives
s(K₂, G) = s(K₂, H) since |V(K₂)| = 2 < 3 ≤ |V|.