Closed walks 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.closed-walks-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.morphisms-undirected-graphs open import graph-theory.polygons open import graph-theory.undirected-graphs
Idea
A closed walk of length k : ℕ
in an undirected graph G
is a morphism of
graphs from a k
-gon into G
.
Definition
module _ {l1 l2 : Level} (k : ℕ) (G : Undirected-Graph l1 l2) where closed-walk-Undirected-Graph : UU (lsuc lzero ⊔ l1 ⊔ l2) closed-walk-Undirected-Graph = Σ (Polygon k) (λ H → hom-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).