Cycle of given length
HasCycleLengthdef
A graph has a cycle of length k when some closed walk of that length repeats no vertex or edge. Which cycle lengths a graph must contain is the subject of a large family of extremal questions.
def HasCycleLength {V : Type*} (G : SimpleGraph V) (k : ℕ) : Prop :=
∃ (v : V) (w : G.Walk v v), w.IsCycle ∧ w.length = kFrom Mathlib
import Conjectura.Defs.Mathematics.Combinatorics.GraphTheory.CycleLength · maintainer — open · raw source
Copyright (c) 2026 The Conjectura Authors. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: The Conjectura Authors