Commit 2026-06-12 00:00 ec04e46e

feat(Combinatorics): define undirected hypergraphs (#28613) This PR defines undirected hypergraphs:

@[ext]
structure Hypergraph (α : Type*) where
  /-- The vertex set -/
  vertexSet : Set α
  /-- The hyperedge set -/
  hyperedgeSet : Set (Set α)
  /-- All hyperedges must be subsets of the vertex set -/
  hyperedge_isSubset_vertexSet : ∀ ⦃e⦄, e ∈ hyperedgeSet → e ⊆ vertexSet

In addition to the main definition, some additional definitions and related lemmas are provided:

• vertex adjacency
• hyperedge adjacency
• vertex "stars"
• special cases (loops, empty hypergraphs, trivial hypergraphs, complete hypergraphs, simple hypergraphs, k-uniform hypergraphs, and d-regular hypergraphs)
• (some) hypergraph cardinality
• subhypergraphs, induced subhypergraphs, and partial hypergraphs This implementation is certainly bare-bones. I'm submitting this PR at this point, rather than when my developments are more fleshed out, because there has been some interest in others contributing to hypergraph formalization in mathlib. In the near future, goals include:
• defining incidence matrices (i.e., conversion from Hypergraph α to Matrix α (Set α) β
• coersion/generalization of graph as 2-uniform hypergraph
• conversion of a hypergraph into its associated clique graph/two-section graph
• constructing the dual of a hypergraph (note: on first blush, this appears somewhat challenging, given that we define hyperedges as Set α rather than some other type β)
• rank and co-rank
• walks, paths, cycles, etc. on hypergraphs