Star Graphs

Main definitions

• SimpleGraph.starGraph r is the star graph on V centered at r. Every non-center vertex is adjacent to r.

Main statements

• SimpleGraph.isTree_starGraph proves the star graph is a tree.

Tags

star graph

def SimpleGraph.starGraph {V : Type u_1} (r : V) : SimpleGraph V

The star graph on V centered at r: every non-center vertex is adjacent to r.

Equations

• SimpleGraph.starGraph r = SimpleGraph.fromRel fun (v x : V) => v = r

@[implicit_reducible]

instance SimpleGraph.instDecidableRelAdjStarGraphOfDecidableEq {V : Type u_1} [DecidableEq V] (r : V) : DecidableRel (starGraph r).Adj

Equations

• SimpleGraph.instDecidableRelAdjStarGraphOfDecidableEq r = SimpleGraph.instDecidableRelAdjStarGraphOfDecidableEq._aux_1 r

@[simp]

theorem SimpleGraph.starGraph_adj {V : Type u_1} {r x y : V} : (starGraph r).Adj x y ↔ x ≠ y ∧ (x = r ∨ y = r)

theorem SimpleGraph.starGraph_adj_center_iff {V : Type u_1} {r v : V} : (starGraph r).Adj r v ↔ r ≠ v

On (starGraph r), r is adjacent to v iff v ≠ r.

theorem SimpleGraph.starGraph_center_adj {V : Type u_1} {r v : V} (h : r ≠ v) : (starGraph r).Adj r v

theorem SimpleGraph.starGraph_center_adj' {V : Type u_1} {r v : V} (h : r ≠ v) : (starGraph r).Adj v r

theorem SimpleGraph.connected_starGraph {V : Type u_1} (r : V) : (starGraph r).Connected

theorem SimpleGraph.isAcyclic_starGraph {V : Type u_1} (r : V) : (starGraph r).IsAcyclic

theorem SimpleGraph.isTree_starGraph {V : Type u_1} (r : V) : (starGraph r).IsTree

theorem SimpleGraph.degree_starGraph_of_ne_center {V : Type u_1} [Fintype V] [DecidableEq V] {r v : V} (h : v ≠ r) : (starGraph r).degree v = 1

Every non-center vertex of a starGraph has degree one.

theorem SimpleGraph.degree_starGraph_center {V : Type u_1} [Fintype V] [DecidableEq V] {r : V} : (starGraph r).degree r = Fintype.card V - 1

The center vertex of a starGraph has degree (card V) - 1.