Documentation

Mathlib.Combinatorics.SimpleGraph.Circulant

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.

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

Circulant graph over additive group G with jumps s

Equations

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

Instances For

@[simp]

theorem SimpleGraph.circulantGraph_adj {G : Type u_1} [AddGroup G] (s : Set G) (a b : G) :

(circulantGraph s).Adj a b = (¬a = b ∧ (a - b ∈ s ∨ b - a ∈ s))

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

circulantGraph s = circulantGraph (s \ {0})

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

circulantGraph s = circulantGraph (s ∪ -s)

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

DecidableRel (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 v d : G} :

(circulantGraph s).Adj (u + d) (v + d) ↔ (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}

Instances For

instance SimpleGraph.instDecidableRelFinAdjCycleGraph (n : ℕ) :

DecidableRel (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 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