Cycles in undirected graphs
Content created by Jonathan Prieto-Cubides, Fredrik Bakke and Egbert Rijke.
Created on 2022-06-15.
Last modified on 2023-03-13.
module graph-theory.cycles-undirected-graphs where
Imports
open import elementary-number-theory.natural-numbers open import foundation.dependent-pair-types open import foundation.universe-levels open import graph-theory.embeddings-undirected-graphs open import graph-theory.polygons open import graph-theory.undirected-graphs
Idea
A cycle in an undirected graph G
consists of a k
-gon H
equipped with an
embedding of graphs from H
into G
.
Definition
module _ {l1 l2 : Level} (k : ℕ) (G : Undirected-Graph l1 l2) where cycle-Undirected-Graph : UU (lsuc lzero ⊔ l1 ⊔ l2) cycle-Undirected-Graph = Σ (Polygon k) (λ H → emb-Undirected-Graph (undirected-graph-Polygon k H) G)
Recent changes
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497). - 2023-03-09. Jonathan Prieto-Cubides. Add hooks (#495).
- 2023-03-07. Fredrik Bakke. Add blank lines between
<details>
tags and markdown syntax (#490). - 2023-03-07. Jonathan Prieto-Cubides. Show module declarations (#488).