Canonical partition into two-vertex edge cliques
DefinitionErdos81_edgePairPartitionchordal-graphsclique-partitioncombinatoricsgraph-theory
For a finite graph , edgePairPartition G is the finite family of all two-element vertex sets that span an edge of . Each member is therefore a two-vertex clique. The family is the canonical one-piece-per-edge candidate for an exact edge-clique partition and provides the baseline against which compression into larger cliques is measured.
Definition code
import Definitions.Def_erdos81_clique_partitions
import Mathlib.Data.Finset.Powerset
namespace Erdos81
universe u
/-- The canonical exact clique partition that treats every edge as a two-vertex clique. -/
noncomputable def edgePairPartition {V : Type u} [Fintype V]
(G : SimpleGraph V) : Finset (Finset V) := by
classical
exact (Finset.univ : Finset V).powerset.filter fun C => C.card = 2 ∧ IsClique G C
end Erdos81Source
Standard graph-theoretic construction: partition an edge set into its individual two-vertex cliques. Introduced as a reusable baseline for the Prove2Me formalization of Erdős Problem 81, https://www.erdosproblems.com/81.