Complete undirected graphs

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides and Vojtěch Štěpančík.

Created on 2022-07-03.
Last modified on 2025-02-11.

module graph-theory.complete-undirected-graphs where
Imports 
open import foundation.universe-levels

open import graph-theory.complete-multipartite-graphs
open import graph-theory.finite-graphs

open import univalent-combinatorics.finite-types

Idea

A complete undirected graph is a complete multipartite graph in which every block has exactly one vertex. In other words, it is an undirected graph in which every vertex is connected to every other vertex.

There are many ways of presenting complete undirected graphs. For example, the type of edges in a complete undirected graph is a 2-element subtype of the type of its vertices.

Definition

complete-Finite-Undirected-Graph :
  {l : Level} → Finite-Type l → Finite-Undirected-Graph l l
complete-Finite-Undirected-Graph X =
  complete-multipartite-Finite-Undirected-Graph X (λ x → unit-Finite-Type)

Recent changes