-- Complete graphs, complements, cliques, and independent sets. -- Part of Cumulus, the Grace17 mathematics library. -- Copyright (c) 2026 Grant Passmore. -- Released under the Apache License 2.0. See LICENSE in the repository root. -- Authors: Grant Passmore module Grace.Cumulus.GraphTheory.Complement import Walks import Cardinal.Countable -- Separation from V × V makes this a set, even for infinite V. def completeEdges (V : Set) : Set := { p ∈ V × V | ∃ x ∈ V, ∃ y ∈ V, p = (x, y) ∧ x ≠ y } theorem completeEdges.adjacent (V x y : Set) shows Adjacent(completeEdges(V), x, y) ↔ (x ∈ V ∧ y ∈ V ∧ x ≠ y) proof constructor . intro edge unfold Adjacent at edge unfold relates at edge simp [completeEdges] at edge rcases edge with ⟨pair, a, ha, b, hb, equality, distinct⟩ obtain ⟨xa, yb⟩ := orderedPair.injective with equality rw ← xa at ha rw ← yb at hb rw [← xa, ← yb] at distinct refine ⟨ha, hb, distinct⟩ . intro h rcases h with ⟨hx, hy, distinct⟩ unfold Adjacent unfold relates simp [completeEdges] have pair := product.pair with hx, hy refine ⟨pair, x, hx, y, hy, rfl, distinct⟩ theorem completeEdges.graph (V : Set) shows SimpleGraph(V, completeEdges(V)) proof constructor intros p hp simp [completeEdges] at hp rcases hp with ⟨pair, witness⟩ exact pair . constructor intros x hx y hy edge have adjacent : Adjacent(completeEdges(V), x, y) by exact edge obtain ⟨hx2, hy2, distinct⟩ := completeEdges.adjacent.forward with adjacent have symmetricEdge : Adjacent(completeEdges(V), y, x) apply completeEdges.adjacent.backward constructor . exact hy . constructor . exact hx . intro equal apply distinct rw equal rfl exact symmetricEdge intros x hx edge have adjacent : Adjacent(completeEdges(V), x, x) by exact edge obtain ⟨hx2, hx3, distinct⟩ := completeEdges.adjacent.forward with adjacent apply distinct rfl theorem SimpleGraph.edges_in_complete (V E : Set) requires graph : SimpleGraph(V, E) shows E ⊆ completeEdges(V) proof intros p hp have relation := SimpleGraph.relation with graph unfold RelationOn at relation unfold RelationBetween at relation have pair := relation with p, hp obtain ⟨bounded, x, hx, y, hy, equality⟩ := product.membership.forward with pair have edge : Adjacent(E, x, y) unfold Adjacent unfold relates rwa ← equality have distinct := Adjacent.distinct with graph, edge have complete : Adjacent(completeEdges(V), x, y) := completeEdges.adjacent.backward with ⟨hx, hy, distinct⟩ unfold Adjacent at complete unfold relates at complete rwa equality def complementEdges (V E : Set) : Set := completeEdges(V) ∖ E theorem complementEdges.membership (V E x y : Set) shows Adjacent(complementEdges(V, E), x, y) ↔ (x ∈ V ∧ y ∈ V ∧ x ≠ y ∧ ¬Adjacent(E, x, y)) proof constructor . intro edge unfold Adjacent at edge unfold relates at edge unfold complementEdges at edge simp [difference.membership] at edge rcases edge with ⟨complete, absent⟩ have adjacent : Adjacent(completeEdges(V), x, y) unfold Adjacent exact complete obtain ⟨hx, hy, distinct⟩ := completeEdges.adjacent.forward with adjacent constructor . exact hx . constructor . exact hy . constructor . exact distinct . intro edge unfold Adjacent at edge apply absent exact edge . intro h rcases h with ⟨hx, hy, distinct, absent⟩ have complete : Adjacent(completeEdges(V), x, y) := completeEdges.adjacent.backward with ⟨hx, hy, distinct⟩ unfold Adjacent at complete unfold Adjacent unfold relates unfold complementEdges apply difference.membership.backward constructor . exact complete . intro edge apply absent unfold Adjacent exact edge theorem complementEdges.graph (V E : Set) requires graph : SimpleGraph(V, E) shows SimpleGraph(V, complementEdges(V, E)) proof constructor intros p hp unfold complementEdges at hp simp [difference.membership] at hp rcases hp with ⟨complete, absent⟩ have relation := SimpleGraph.relation at V, completeEdges(V) with completeEdges.graph at V unfold RelationOn at relation unfold RelationBetween at relation exact relation with p, complete . constructor intros x hx y hy edge have adjacent : Adjacent(complementEdges(V, E), x, y) by exact edge obtain ⟨hx2, hy2, distinct, absent⟩ := complementEdges.membership.forward with adjacent have reverseEdge : Adjacent(complementEdges(V, E), y, x) apply complementEdges.membership.backward constructor . exact hy . constructor . exact hx . constructor . intro equal apply distinct rw equal rfl . intro reverse have forward := Adjacent.symmetric with graph, reverse apply absent exact forward exact reverseEdge intros x hx edge have adjacent : Adjacent(complementEdges(V, E), x, x) by exact edge obtain ⟨hx2, hx3, distinct, absent⟩ := complementEdges.membership.forward with adjacent apply distinct rfl predicate Clique (V E S : Set) := S ⊆ V ∧ (∀ x ∈ S, ∀ y ∈ S, x ≠ y → Adjacent(E, x, y)) predicate Independent (V E S : Set) := S ⊆ V ∧ (∀ x ∈ S, ∀ y ∈ S, ¬Adjacent(E, x, y)) theorem Independent.in_complement (V E S : Set) requires independent : Independent(V, E, S) shows Clique(V, complementEdges(V, E), S) proof rcases independent with ⟨included, noEdges⟩ constructor . exact included . intros x hx y hy distinct have xInV := included with x, hx have yInV := included with y, hy have absent := noEdges with x, hx, y, hy exact complementEdges.membership.backward with ⟨xInV, yInV, distinct, absent⟩ theorem Clique.in_complement (V E S : Set) requires clique : Clique(V, complementEdges(V, E), S) requires graph : SimpleGraph(V, E) shows Independent(V, E, S) proof rcases clique with ⟨included, allEdges⟩ constructor . exact included . intros x hx y hy edge have distinct := Adjacent.distinct with graph, edge have complementary := allEdges with x, hx, y, hy, distinct obtain ⟨xInV, yInV, d, absent⟩ := complementEdges.membership.forward with complementary apply absent exact edge theorem complementEdges.involution (V E : Set) requires graph : SimpleGraph(V, E) shows complementEdges(V, complementEdges(V, E)) = E proof ext p have included := SimpleGraph.edges_in_complete with graph have membership : p ∈ E → p ∈ completeEdges(V) intro hp exact included with p, hp constructor . intro h unfold complementEdges at h obtain ⟨inComplete, notInner⟩ := difference.membership.forward with h have cases : p ∈ E ∨ ¬(p ∈ E) by tauto cases cases with yes | no . exact yes . exfalso apply notInner exact difference.membership.backward with ⟨inComplete, no⟩ . intro he unfold complementEdges apply difference.membership.backward constructor . exact membership with he . intro inner obtain ⟨inComplete, absent⟩ := difference.membership.forward with inner apply absent exact he def independentSets (V E : Set) : Set := { S ∈ 𝒫(V) | Independent(V, E, S) } theorem independentSets.empty_graph (V : Set) shows independentSets(V, empty) = 𝒫(V) proof ext S constructor . intro h simp [independentSets] at h rcases h with ⟨inPower, independent⟩ exact inPower . intro inPower have subset := set.powerset.forward with inPower simp [independentSets] constructor . exact inPower constructor . unfold Subset exact subset . intros x hx y hy edge unfold Adjacent at edge unfold relates at edge exact set.empty with edge -- Cantor's diagonal argument has a graph-theoretic consequence even when -- there are no edges: the independent vertex subsets cannot be enumerated -- by the vertices themselves. theorem Independent.no_surjection_from_vertices (V f : Set) shows ¬SurjectiveBetween(f, V, independentSets(V, empty)) proof intro onto have allSubsets := independentSets.empty_graph at V rw allSubsets at onto exact Cantor.no_surjection_onto_powerset with onto