Undirected hypergraphs

An undirected hypergraph (here abbreviated as hypergraph) H is a generalization of a graph (see Mathlib.Combinatorics.Graph or Mathlib.Combinatorics.SimpleGraph) and consists of a set of vertices, usually denoted V or V(H), and a set of hyperedges, here called edges and denoted E or E(H). In contrast with a graph, where edges are unordered pairs of vertices, in hypergraphs, edges are unordered sets of vertices; i.e., they are subsets of the vertex set V.

A hypergraph where V = ∅ and E = ∅ is empty, denoted ⊥. A hypergraph with a nonempty vertex set (V ≠ ∅) and empty edge set is trivial. A hypergraph where the edge set is the power set of the vertex set (or, equivalently, where all possible subsets of the vertex sets are in the edge set) is complete.

If a edge e contains only one vertex (i.e., |e| = 1), then it is a loop.

This module defines Hypergraph α for a vertex type α (edges are defined as Set (Set α)).

Main definitions

• Hypergraph α is the type of undirected hypergraphs with vertices of type α and edges of type Set α. In addition to vertices and hyperedges, a Hypergraph must have the property that all edges are subsets of the vertex set.

For H : Hypergraph α:

• H.vertexSet (abbrev. V(H)) denotes the vertex set of H as a term in Set α.
• H.edgeSet (abbrev. E(H)) denotes the edge set of H as a term in Set (Set α). Hyperedges must be subsets of V(H).
• H.Adj x y means that there exists some edge containing both x and y (or, in other words, x and y are incident to some shared edge e).
• H.EAdj e f means that there exists some vertex that is incident to the edges e and f : Set α.

Implementation details

This implementation is heavily inspired by Peter Nelson and Jun Kwon's Graph implementation, which was in turn inspired by Matroid.

Paraphrasing Mathlib.Combinatorics.Graph.Basic: "The main tradeoff is that parts of the API will need to care about whether a term x : α or e : Set α is a 'real' vertex or edge of the graph, rather than something outside the vertex or edge set. This is an issue, but is likely amenable to automation."

Because edgeSet is a Set (Set α), rather than a multiset, here we are assuming that all hypergraphs are without repeated edge.

structure Hypergraph (α : Type u_4) : Type u_4

An undirected hypergraph with vertices of type α and edges of type Set α, as described by vertex and edge sets vertexSet : Set α and edgeSet : Set (Set α).

The requirement subset_vertexSet_of_mem_edgeSet ensures that all vertices in edges are part of vertexSet, i.e., all edges are subsets of the vertexSet.

• vertexSet : Set α

  The vertex set

• edgeSet : Set (Set α)

  The edge set

• subset_vertexSet_of_mem_edgeSet' ⦃e : Set α⦄ : e ∈ self.edgeSet → e ⊆ self.vertexSet

  All edges must be subsets of the vertex set

theorem Hypergraph.ext {α : Type u_4} {x y : Hypergraph α} (vertexSet : x.vertexSet = y.vertexSet) (edgeSet : x.edgeSet = y.edgeSet) : x = y

theorem Hypergraph.ext_iff {α : Type u_4} {x y : Hypergraph α} : x = y ↔ x.vertexSet = y.vertexSet ∧ x.edgeSet = y.edgeSet

Notation

def Hypergraph.«termV(_)» : Lean.ParserDescr

V(H) denotes the vertexSet of a hypergraph H

Equations

• One or more equations did not get rendered due to their size.

def Hypergraph.«termE(_)» : Lean.ParserDescr

E(H) denotes the edgeSet of a hypergraph H

Equations

• One or more equations did not get rendered due to their size.

Vertex-Hyperedge Incidence

@[simp]

theorem Hypergraph.subset_vertexSet_of_mem_edgeSet {α : Type u_1} {e : Set α} {H : Hypergraph α} (he : e ∈ H.edgeSet) : e ⊆ H.vertexSet

theorem Membership.mem.subset_vertexSet {α : Type u_1} {e : Set α} {H : Hypergraph α} (he : e ∈ H.edgeSet) : e ⊆ H.vertexSet

Alias of Hypergraph.subset_vertexSet_of_mem_edgeSet.

theorem Hypergraph.edgeSet_subset_powerset_vertexSet {α : Type u_1} {H : Hypergraph α} : H.edgeSet ⊆ 𝒫 H.vertexSet

theorem Hypergraph.mem_vertexSet_of_mem_edgeSet {α : Type u_1} {x : α} {e : Set α} {H : Hypergraph α} (he : e ∈ H.edgeSet) (hx : x ∈ e) : x ∈ H.vertexSet

theorem Hypergraph.edgeSet.ext_iff {α : Type u_1} {e e' : Set α} {H : Hypergraph α} (he : e ∈ H.edgeSet) (he' : e' ∈ H.edgeSet) : e = e' ↔ ∀ x ∈ H.vertexSet, x ∈ e ↔ x ∈ e'

theorem Hypergraph.sUnion_edgeSet_subset_vertexSet {α : Type u_1} {H : Hypergraph α} : ⋃₀ H.edgeSet ⊆ H.vertexSet

Vertex and Hyperedge Adjacency

def Hypergraph.Adj {α : Type u_1} (H : Hypergraph α) (x y : α) : Prop

Predicate for adjacency. Two vertices x and y are adjacent if there is some edge e ∈ E(H) where x and y are both incident to e.

Note that we do not need to explicitly check that x, y ∈ V(H) here because a vertex that is not in the vertex set cannot be incident to any edge.

Equations

• H.Adj x y = ∃ e ∈ H.edgeSet, x ∈ e ∧ y ∈ e

theorem Hypergraph.Adj.symm {α : Type u_1} {x y : α} {H : Hypergraph α} (h : H.Adj x y) : H.Adj y x

theorem Hypergraph.adj_comm {α : Type u_1} {H : Hypergraph α} (x y : α) : H.Adj x y ↔ H.Adj y x

def Hypergraph.EAdj {α : Type u_1} (H : Hypergraph α) (e f : Set α) : Prop

Predicate for edge adjacency. Analogous to Hypergraph.Adj, edges e and f are adjacent if there is some vertex x ∈ V(H) where x is incident to both e and f.

Equations

• H.EAdj e f = (e ∈ H.edgeSet ∧ f ∈ H.edgeSet ∧ ∃ x ∈ e, x ∈ f)

theorem Hypergraph.EAdj.exists_vertex {α : Type u_1} {e f : Set α} {H : Hypergraph α} (h : H.EAdj e f) : ∃ x ∈ H.vertexSet, x ∈ e ∧ x ∈ f

theorem Hypergraph.EAdj.symm {α : Type u_1} {e f : Set α} {H : Hypergraph α} (h : H.EAdj e f) : H.EAdj f e

theorem Hypergraph.EAdj.inter_nonempty {α : Type u_1} {e f : Set α} {H : Hypergraph α} (hef : H.EAdj e f) : (e ∩ f).Nonempty

theorem Hypergraph.eAdj_comm {α : Type u_1} {H : Hypergraph α} (e f : Set α) : H.EAdj e f ↔ H.EAdj f e

Basic Hypergraph Definitions & Predicates

def Hypergraph.image {α : Type u_1} {β : Type u_2} (H : Hypergraph α) (f : α → β) : Hypergraph β

The image of a hypergraph H : Hypergraph α under a function f : α → β is the hypergraph Hᶠ : Hypergraph β where the vertex set of Hᶠ is the image of V(H) under f and the edge set of Hᶠ is the set of images of the edges (subsets of vertices) in E(H).

Equations

• H.image f = { vertexSet := f '' H.vertexSet, edgeSet := Set.image f '' H.edgeSet, subset_vertexSet_of_mem_edgeSet' := ⋯ }

@[simp]

theorem Hypergraph.image_vertexSet {α : Type u_1} {β : Type u_2} (H : Hypergraph α) (f : α → β) : (H.image f).vertexSet = f '' H.vertexSet

@[simp]

theorem Hypergraph.image_edgeSet {α : Type u_1} {β : Type u_2} (H : Hypergraph α) (f : α → β) : (H.image f).edgeSet = Set.image f '' H.edgeSet

theorem Hypergraph.mem_edgeSet_image {α : Type u_1} {β : Type u_2} {H : Hypergraph α} {f : α → β} {e : Set β} : e ∈ (H.image f).edgeSet ↔ ∃ e' ∈ H.edgeSet, f '' e' = e

theorem Hypergraph.image_mem_edgeSet_image {α : Type u_1} {β : Type u_2} {e : Set α} {H : Hypergraph α} {f : α → β} (he : e ∈ H.edgeSet) : f '' e ∈ (H.image f).edgeSet

theorem Hypergraph.image_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → γ} (H : Hypergraph α) : (H.image f).image g = H.image (g ∘ f)

def Hypergraph.IsIsolated {α : Type u_1} (H : Hypergraph α) (x : α) : Prop

A vertex is isolated if it is not incident to any edges (including loops).

Equations

• H.IsIsolated x = ∀ e ∈ H.edgeSet, x ∉ e

theorem Hypergraph.sUnion_edgeSet_eq_vertexSet_iff_all_vertex_not_isolated {α : Type u_1} {H : Hypergraph α} : ⋃₀ H.edgeSet = H.vertexSet ↔ ∀ x ∈ H.vertexSet, ¬H.IsIsolated x

def Hypergraph.IsLoop {α : Type u_1} (H : Hypergraph α) (e : Set α) : Prop

A loop is an edge whose associated vertex subset consists of a single vertex.

Equations

• H.IsLoop e = (e ∈ H.edgeSet ∧ ∃ (x : α), e = {x})

theorem Hypergraph.isLoop_iff_mem_edgeSet_and_singleton {α : Type u_1} {e : Set α} {H : Hypergraph α} : H.IsLoop e ↔ e ∈ H.edgeSet ∧ ∃ (x : α), e = {x}

theorem Hypergraph.isLoop_iff_mem_and_ncard_one {α : Type u_1} {e : Set α} {H : Hypergraph α} : H.IsLoop e ↔ e ∈ H.edgeSet ∧ e.ncard = 1

theorem Hypergraph.IsLoop.ncard_one {α : Type u_1} {e : Set α} {H : Hypergraph α} (h : H.IsLoop e) : e.ncard = 1

def Hypergraph.IsNonempty {α : Type u_1} (H : Hypergraph α) : Prop

A hypergraph is nonempty if it has at least one vertex or at least one edge.

Equations

• H.IsNonempty = (H.vertexSet.Nonempty ∨ H.edgeSet.Nonempty)

@[implicit_reducible]

instance Hypergraph.instBot (α : Type u_4) : Bot (Hypergraph α)

The empty hypergraph (bottom) on a type.

Equations

• Hypergraph.instBot α = { bot := { vertexSet := ∅, edgeSet := ∅, subset_vertexSet_of_mem_edgeSet' := ⋯ } }

@[simp]

theorem Hypergraph.bot_vertexSet (α : Type u_4) : ⊥.vertexSet = ∅

@[simp]

theorem Hypergraph.bot_edgeSet (α : Type u_4) : ⊥.edgeSet = ∅

@[simp]

theorem Hypergraph.IsNonempty.of_nonempty_vertexSet {α : Type u_1} {H : Hypergraph α} (hV : H.vertexSet.Nonempty) : H.IsNonempty

@[simp]

theorem Hypergraph.IsNonempty.of_nonempty_edgeSet {α : Type u_1} {H : Hypergraph α} (hE : H.edgeSet.Nonempty) : H.IsNonempty

@[simp]

theorem Hypergraph.ne_bot_iff {α : Type u_1} {H : Hypergraph α} : H ≠ ⊥ ↔ H.IsNonempty

theorem Hypergraph.IsNonempty.ne_bot {α : Type u_1} {H : Hypergraph α} : H.IsNonempty → H ≠ ⊥

Alias of the reverse direction of Hypergraph.ne_bot_iff.

@[simp]

theorem Hypergraph.not_isNonempty_iff {α : Type u_1} {H : Hypergraph α} : ¬H.IsNonempty ↔ H = ⊥

theorem Hypergraph.eq_bot_or_isNonempty {α : Type u_1} (H : Hypergraph α) : H = ⊥ ∨ H.IsNonempty

def Hypergraph.IsTrivial {α : Type u_1} (H : Hypergraph α) : Prop

A hypergraph is trivial if it has at least one vertex but no edges.

Equations

• H.IsTrivial = (H.vertexSet.Nonempty ∧ H.edgeSet = ∅)

def Hypergraph.trivialOn {α : Type u_1} (f : Set α) : Hypergraph α

The trivial hypergraph with a given vertex set is defined by having no edges on that vertex set.

Equations

• Hypergraph.trivialOn f = { vertexSet := f, edgeSet := ∅, subset_vertexSet_of_mem_edgeSet' := ⋯ }

@[simp]

theorem Hypergraph.trivialOn_edgeSet {α : Type u_1} (f : Set α) : (trivialOn f).edgeSet = ∅

@[simp]

theorem Hypergraph.trivialOn_vertexSet {α : Type u_1} (f : Set α) : (trivialOn f).vertexSet = f

theorem Hypergraph.IsTrivial.trivialOn {α : Type u_1} {f : Set α} (hf : f.Nonempty) : (Hypergraph.trivialOn f).IsTrivial

theorem Hypergraph.IsTrivial.isNonempty {α : Type u_1} {H : Hypergraph α} (h : H.IsTrivial) : H.IsNonempty

theorem Hypergraph.IsTrivial.not_mem_edgeSet {α : Type u_1} {e : Set α} {H : Hypergraph α} (h : H.IsTrivial) : e ∉ H.edgeSet

def Hypergraph.IsComplete {α : Type u_1} (H : Hypergraph α) : Prop

A hypergraph is complete if every subset of the vertex set is in the edge set.

Equations

• H.IsComplete = ∀ e ⊆ H.vertexSet, e ∈ H.edgeSet

def Hypergraph.completeOn {α : Type u_1} (f : Set α) : Hypergraph α

The complete hypergraph with a given vertex set, which has each subset of the vertex set as an edge.

Equations

• Hypergraph.completeOn f = { vertexSet := f, edgeSet := 𝒫 f, subset_vertexSet_of_mem_edgeSet' := ⋯ }

@[simp]

theorem Hypergraph.completeOn_vertexSet {α : Type u_1} (f : Set α) : (completeOn f).vertexSet = f

@[simp]

theorem Hypergraph.completeOn_edgeSet {α : Type u_1} (f : Set α) : (completeOn f).edgeSet = 𝒫 f

theorem Hypergraph.mem_completeOn {α : Type u_1} {e f : Set α} : e ∈ (completeOn f).edgeSet ↔ e ⊆ f

theorem Hypergraph.IsComplete.mem_iff {α : Type u_1} {e : Set α} {H : Hypergraph α} (h : H.IsComplete) : e ∈ H.edgeSet ↔ e ⊆ H.vertexSet

theorem Hypergraph.IsComplete.completeOn {α : Type u_1} (f : Set α) : (Hypergraph.completeOn f).IsComplete

theorem Hypergraph.IsComplete.isNonempty {α : Type u_1} {H : Hypergraph α} (h : H.IsComplete) : H.IsNonempty

theorem Hypergraph.IsComplete.not_isTrivial {α : Type u_1} {H : Hypergraph α} (h : H.IsComplete) : ¬H.IsTrivial

theorem Hypergraph.not_isTrivial_completeOn {α : Type u_1} (f : Set α) : ¬(completeOn f).IsTrivial