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

Equations

• SimpleGraph.cycleGraph 0 = ⊥
• SimpleGraph.cycleGraph 1 = ⊥
• SimpleGraph.cycleGraph n.succ.succ = { Adj := fun (a b : Fin (n + 2)) => a - b = 1 ∨ b - a = 1, symm := ⋯, loopless := ⋯ }

@[instance_reducible]

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

Equations

• SimpleGraph.instDecidableRelFinAdjCycleGraph 0 = fun (x x_1 : Fin 0) => { decide := false, reflects_decide := ⋯ }
• SimpleGraph.instDecidableRelFinAdjCycleGraph 1 = fun (x x_1 : Fin 1) => { decide := false, reflects_decide := ⋯ }
• SimpleGraph.instDecidableRelFinAdjCycleGraph n.succ.succ = id inferInstance

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_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_eq_top_iff {n : ℕ} : cycleGraph n = ⊤ ↔ n ≤ 3

theorem SimpleGraph.cycleGraph_two_eq_top : cycleGraph 2 = ⊤

theorem SimpleGraph.cycleGraph_three_eq_top : cycleGraph 3 = ⊤

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

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

The Eulerian cycle of cycleGraph (n + 3)

Equations

• SimpleGraph.cycleGraph.cycle n = SimpleGraph.Walk.cons ⋯ (SimpleGraph.cycleGraph.cycleCons✝ n (Fin.last (n + 2)))

@[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.mem_support_cycle {n : ℕ} (u : Fin (n + 3)) : u ∈ (cycle n).support

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.

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