Graph theory

Content created by Egbert Rijke, Fredrik Bakke and Jonathan Prieto-Cubides.

Created on 2022-03-12.
Last modified on 2024-12-03.

Modules in the graph theory namespace

module graph-theory where

open import graph-theory.acyclic-undirected-graphs public
open import graph-theory.base-change-dependent-directed-graphs public
open import graph-theory.base-change-dependent-reflexive-graphs public
open import graph-theory.cartesian-products-directed-graphs public
open import graph-theory.cartesian-products-reflexive-graphs public
open import graph-theory.circuits-undirected-graphs public
open import graph-theory.closed-walks-undirected-graphs public
open import graph-theory.complete-bipartite-graphs public
open import graph-theory.complete-multipartite-graphs public
open import graph-theory.complete-undirected-graphs public
open import graph-theory.connected-undirected-graphs public
open import graph-theory.cycles-undirected-graphs public
open import graph-theory.dependent-directed-graphs public
open import graph-theory.dependent-products-directed-graphs public
open import graph-theory.dependent-products-reflexive-graphs public
open import graph-theory.dependent-reflexive-graphs public
open import graph-theory.dependent-sums-directed-graphs public
open import graph-theory.dependent-sums-reflexive-graphs public
open import graph-theory.directed-graph-duality public
open import graph-theory.directed-graph-structures-on-standard-finite-sets public
open import graph-theory.directed-graphs public
open import graph-theory.discrete-dependent-reflexive-graphs public
open import graph-theory.discrete-directed-graphs public
open import graph-theory.discrete-reflexive-graphs public
open import graph-theory.displayed-large-reflexive-graphs public
open import graph-theory.edge-coloured-undirected-graphs public
open import graph-theory.embeddings-directed-graphs public
open import graph-theory.embeddings-undirected-graphs public
open import graph-theory.enriched-undirected-graphs public
open import graph-theory.equivalences-dependent-directed-graphs public
open import graph-theory.equivalences-dependent-reflexive-graphs public
open import graph-theory.equivalences-directed-graphs public
open import graph-theory.equivalences-enriched-undirected-graphs public
open import graph-theory.equivalences-reflexive-graphs public
open import graph-theory.equivalences-undirected-graphs public
open import graph-theory.eulerian-circuits-undirected-graphs public
open import graph-theory.faithful-morphisms-undirected-graphs public
open import graph-theory.fibers-directed-graphs public
open import graph-theory.fibers-morphisms-directed-graphs public
open import graph-theory.fibers-morphisms-reflexive-graphs public
open import graph-theory.finite-graphs public
open import graph-theory.geometric-realizations-undirected-graphs public
open import graph-theory.higher-directed-graphs public
open import graph-theory.hypergraphs public
open import graph-theory.internal-hom-directed-graphs public
open import graph-theory.large-higher-directed-graphs public
open import graph-theory.large-reflexive-graphs public
open import graph-theory.matchings public
open import graph-theory.mere-equivalences-undirected-graphs public
open import graph-theory.morphisms-dependent-directed-graphs public
open import graph-theory.morphisms-directed-graphs public
open import graph-theory.morphisms-reflexive-graphs public
open import graph-theory.morphisms-undirected-graphs public
open import graph-theory.neighbors-undirected-graphs public
open import graph-theory.orientations-undirected-graphs public
open import graph-theory.paths-undirected-graphs public
open import graph-theory.polygons public
open import graph-theory.raising-universe-levels-directed-graphs public
open import graph-theory.reflecting-maps-undirected-graphs public
open import graph-theory.reflexive-graphs public
open import graph-theory.regular-undirected-graphs public
open import graph-theory.sections-dependent-directed-graphs public
open import graph-theory.sections-dependent-reflexive-graphs public
open import graph-theory.simple-undirected-graphs public
open import graph-theory.stereoisomerism-enriched-undirected-graphs public
open import graph-theory.terminal-directed-graphs public
open import graph-theory.terminal-reflexive-graphs public
open import graph-theory.totally-faithful-morphisms-undirected-graphs public
open import graph-theory.trails-directed-graphs public
open import graph-theory.trails-undirected-graphs public
open import graph-theory.undirected-graph-structures-on-standard-finite-sets public
open import graph-theory.undirected-graphs public
open import graph-theory.universal-directed-graph public
open import graph-theory.universal-reflexive-graph public
open import graph-theory.vertex-covers public
open import graph-theory.voltage-graphs public
open import graph-theory.walks-directed-graphs public
open import graph-theory.walks-undirected-graphs public
open import graph-theory.wide-displayed-large-reflexive-graphs public

Recent changes