Documentation

Mathlib.Combinatorics.SimpleGraph.CycleGraph

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 := ⋯ }

Instances For

@[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_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.cycleGraph_preconnected {n : ℕ} :

(cycleGraph n).Preconnected

theorem SimpleGraph.cycleGraph_connected {n : ℕ} :

(cycleGraph (n + 1)).Connected

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)))

Instances For

@[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