Simplex graphs

DefinitionSimplex vertices#✓fully proved

Let \(G\) be a simple graph on a vertex type \(V\). A simplex vertex of \(G\) is a finite set \(s\) of vertices that is a clique of \(G\), meaning that any two distinct elements of \(s\) are adjacent in \(G\).

public def SimplexVertex := { s : Finset V // G.IsClique (↑s : Set V) }

Used by 5

Used byAdjacency in the simplex graph · The empty clique is adjacent to every singleton · Empty simplex vertex · Simplex graph · Singleton simplex vertex

DefinitionEmpty simplex vertex#✓fully proved

Let \(G\) be a simple graph. The empty simplex vertex of \(G\) is the empty set of vertices, which is a clique of \(G\).

public def emptyVertex : SimplexVertex G := ⟨∅, by simp⟩

Uses 1 · Used by 1

Statement usesSimplex vertices

Used byThe empty clique is adjacent to every singleton

DefinitionSingleton simplex vertex#✓fully proved

Let \(G\) be a simple graph. For a vertex \(v\) of \(G\), the singleton simplex vertex of \(v\) is the one-element set containing \(v\), which is a clique of \(G\).

public def singletonVertex (v : V) : SimplexVertex G := ⟨{v}, by simp⟩

Uses 1 · Used by 1

Statement usesSimplex vertices

Used byThe empty clique is adjacent to every singleton

DefinitionSimplex graph#✓fully proved

Let \(G\) be a simple graph. The simplex graph of \(G\) is the simple graph whose vertices are the simplex vertices of \(G\) (the finite cliques of \(G\)), in which two cliques \(s\) and \(t\) are adjacent exactly when their symmetric difference \(s \triangle t\) has exactly one element.

The vertex type of \(G\) is not required to be finite.

public def simplexGraph : SimpleGraph (SimplexVertex G) where
  Adj x y := (x.val ∆ y.val).card = 1
  symm := ⟨by
    intro x y h
    simpa only [symmDiff_comm] using h⟩
  loopless := ⟨by
    intro x h
    rw [Finset.symmDiff_def] at h
    simp at h⟩

Uses 1 · Used by 2

Statement usesSimplex vertices

Used byAdjacency in the simplex graph · The empty clique is adjacent to every singleton

TheoremAdjacency in the simplex graph#✓fully proved

Let \(G\) be a simple graph. Two simplex vertices \(s\) and \(t\) of \(G\) are adjacent in the simplex graph of \(G\) if and only if their symmetric difference \(s \triangle t\) has exactly one element.

public theorem adj_iff (x y : SimplexVertex G) :
    (simplexGraph G).Adj x y ↔ (x.val ∆ y.val).card = 1

Uses 2

Statement usesSimplex vertices · Simplex graph

TheoremThe empty clique is adjacent to every singleton#✓fully proved

Let \(G\) be a simple graph. For every vertex \(v\) of \(G\), the empty simplex vertex of \(G\) and the singleton simplex vertex of \(v\) are adjacent in the simplex graph of \(G\).

public theorem empty_adj_singleton (v : V) :
    (simplexGraph G).Adj (emptyVertex G) (singletonVertex G v)

Uses 4

Statement usesSimplex vertices · Empty simplex vertex · Simplex graph · Singleton simplex vertex

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.