Definition of circulant graphs

This file defines and proves several fact about circulant graphs. A circulant graph over type G with jumps s : Set G is a graph in which two vertices u and v are adjacent if and only if u - v ∈ s or v - u ∈ s. The elements of s are called jumps.

Main declarations

• SimpleGraph.circulantGraph s: the circulant graph over G with jumps s.
• SimpleGraph.cycleGraph n: the cycle graph over Fin n.

@[simp]

theorem SimpleGraph.circulantGraph_adj {G : Type u_1} [AddGroup G] (s : Set G) (a : G) (b : G) : (SimpleGraph.circulantGraph s).Adj a b = (¬a = b ∧ (a - b ∈ s ∨ b - a ∈ s))

def SimpleGraph.circulantGraph {G : Type u_1} [AddGroup G] (s : Set G) : SimpleGraph G

Circulant graph over additive group G with jumps s

Equations

• SimpleGraph.circulantGraph s = SimpleGraph.fromRel fun (x1 x2 : G) => x1 - x2 ∈ s

theorem SimpleGraph.circulantGraph_eq_erase_zero {G : Type u_1} [AddGroup G] (s : Set G) : SimpleGraph.circulantGraph s = SimpleGraph.circulantGraph (s \ {0})

theorem SimpleGraph.circulantGraph_eq_symm {G : Type u_1} [AddGroup G] (s : Set G) : SimpleGraph.circulantGraph s = SimpleGraph.circulantGraph (s ∪ -s)

instance SimpleGraph.instDecidableRelAdjCirculantGraphOfDecidableEqOfDecidablePredMemSet {G : Type u_1} [AddGroup G] (s : Set G) [DecidableEq G] [DecidablePred fun (x : G) => x ∈ s] : DecidableRel (SimpleGraph.circulantGraph s).Adj

Equations

• One or more equations did not get rendered due to their size.

theorem SimpleGraph.circulantGraph_adj_translate {G : Type u_1} [AddGroup G] {s : Set G} {u : G} {v : G} {d : G} : (SimpleGraph.circulantGraph s).Adj (u + d) (v + d) ↔ (SimpleGraph.circulantGraph s).Adj u v

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

Cycle graph over Fin n

Equations

• SimpleGraph.cycleGraph 0 = ⊥
• SimpleGraph.cycleGraph n.succ = SimpleGraph.circulantGraph {1}

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

Equations

• SimpleGraph.instDecidableRelFinAdjCycleGraph 0 = fun (x x : Fin 0) => inferInstanceAs (Decidable False)
• SimpleGraph.instDecidableRelFinAdjCycleGraph n.succ = inferInstanceAs (DecidableRel (SimpleGraph.circulantGraph {1}).Adj)

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

theorem SimpleGraph.cycleGraph_zero_eq_bot : SimpleGraph.cycleGraph 0 = ⊥

theorem SimpleGraph.cycleGraph_one_eq_bot : SimpleGraph.cycleGraph 1 = ⊥

theorem SimpleGraph.cycleGraph_zero_eq_top : SimpleGraph.cycleGraph 0 = ⊤

theorem SimpleGraph.cycleGraph_one_eq_top : SimpleGraph.cycleGraph 1 = ⊤

theorem SimpleGraph.cycleGraph_two_eq_top : SimpleGraph.cycleGraph 2 = ⊤

theorem SimpleGraph.cycleGraph_three_eq_top : SimpleGraph.cycleGraph 3 = ⊤

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

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

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

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

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

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

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

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

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

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