Definition of cycle graphs

This file defines and proves several fact about cycle graphs on n vertices and the cycle around the cycle graph when n ≥ 3.

Main declarations

• SimpleGraph.cycleGraph n: the cycle graph over Fin n.
• (SimpleGraph.cycleGraph n).cycle: the cycle around cycleGraph (n + 3) starting at 0.

def SimpleGraph.cycleGraph (n : ℕ) : SimpleGraph (Fin n)

Cycle graph over Fin n

@[instance_reducible]

instance SimpleGraph.instDecidableRelFinAdjCycleGraph (n : ℕ) : DecidableRel (cycleGraph n).Adj

theorem SimpleGraph.cycleGraph_zero_adj {u v : Fin 0} : ¬(cycleGraph 0).Adj u v

theorem SimpleGraph.cycleGraph_zero_eq_bot : cycleGraph 0 = ⊥

theorem SimpleGraph.cycleGraph_one_eq_bot : cycleGraph 1 = ⊥

theorem SimpleGraph.cycleGraph_zero_eq_top : cycleGraph 0 = ⊤

theorem SimpleGraph.cycleGraph_one_eq_top : cycleGraph 1 = ⊤

theorem SimpleGraph.cycleGraph_two_eq_top : cycleGraph 2 = ⊤

theorem SimpleGraph.cycleGraph_three_eq_top : cycleGraph 3 = ⊤

theorem SimpleGraph.cycleGraph_one_adj {u v : Fin 1} : ¬(cycleGraph 1).Adj u v

theorem SimpleGraph.cycleGraph_adj {n : ℕ} {u v : Fin (n + 2)} : (cycleGraph (n + 2)).Adj u v ↔ u - v = 1 ∨ v - u = 1

theorem SimpleGraph.cycleGraph_adj' {n : ℕ} {u v : Fin n} : (cycleGraph n).Adj u v ↔ ↑(u - v) = 1 ∨ ↑(v - u) = 1

theorem SimpleGraph.cycleGraph_neighborSet {n : ℕ} {v : Fin (n + 2)} : (cycleGraph (n + 2)).neighborSet v = {v - 1, v + 1}

theorem SimpleGraph.cycleGraph_neighborFinset {n : ℕ} {v : Fin (n + 2)} : (cycleGraph (n + 2)).neighborFinset v = {v - 1, v + 1}

theorem SimpleGraph.cycleGraph_degree_two_le {n : ℕ} {v : Fin (n + 2)} : (cycleGraph (n + 2)).degree v = {v - 1, v + 1}.card

theorem SimpleGraph.cycleGraph_degree_three_le {n : ℕ} {v : Fin (n + 3)} : (cycleGraph (n + 3)).degree v = 2

theorem SimpleGraph.pathGraph_le_cycleGraph {n : ℕ} : pathGraph n ≤ cycleGraph n

theorem SimpleGraph.preconnected_cycleGraph {n : ℕ} : (cycleGraph n).Preconnected

@[deprecated SimpleGraph.preconnected_cycleGraph (since := "2026-10-01")]

theorem SimpleGraph.cycleGraph_preconnected {n : ℕ} : (cycleGraph n).Preconnected

Alias of SimpleGraph.preconnected_cycleGraph.

theorem SimpleGraph.connected_cycleGraph_add_one {n : ℕ} : (cycleGraph (n + 1)).Connected

@[deprecated SimpleGraph.connected_cycleGraph_add_one (since := "2026-10-01")]

theorem SimpleGraph.cycleGraph_connected {n : ℕ} : (cycleGraph (n + 1)).Connected

Alias of SimpleGraph.connected_cycleGraph_add_one.

def SimpleGraph.cycleGraph.cycle (n : ℕ) : (cycleGraph (n + 3)).Walk 0 0

The Eulerian cycle of cycleGraph (n + 3)

@[simp]

theorem SimpleGraph.cycleGraph.length_cycle {n : ℕ} : (cycle n).length = n + 3

theorem SimpleGraph.cycleGraph.getVert_cycle {n m : ℕ} (hm : m ≤ n + 3) : (cycle n).getVert m = ⟨(n + 3 - m) % (n + 3), ⋯⟩

theorem SimpleGraph.cycleGraph.isPath_tail_cycle {n : ℕ} : (cycle n).tail.IsPath

theorem SimpleGraph.cycleGraph.isCycle_cycle {n : ℕ} : (cycle n).IsCycle

theorem SimpleGraph.cycleGraph_isContained_iff {V : Type u_1} {G : SimpleGraph V} {n : ℕ} (hn : 2 < n) : (cycleGraph n).IsContained G ↔ ∃ (v : V) (p : G.Walk v v), p.IsCycle ∧ p.length = n