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

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

@[simp]

theorem SimpleGraph.isUniversal_starGraph_self {V : Type u_1} {r : V} : (starGraph r).IsUniversal r

theorem SimpleGraph.starGraph_le_iff {V : Type u_1} {G : SimpleGraph V} {r : V} : starGraph r ≤ G ↔ G.IsUniversal 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

def SimpleGraph.Coloring.starGraphBool {V : Type u_1} (r : V) [DecidableEq V] : (starGraph r).Coloring Bool

Bicoloring of a star graph

Equations

• SimpleGraph.Coloring.starGraphBool r = { toFun := fun (v : V) => decide (v = r), map_rel' := ⋯ }

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

theorem SimpleGraph.IsBipartiteWith.starGraph {V : Type u_1} (r : V) : (SimpleGraph.starGraph r).IsBipartiteWith {r} {r}ᶜ

theorem SimpleGraph.IsCompleteBetween.starGraph {V : Type u_1} (r : V) : (SimpleGraph.starGraph r).IsCompleteBetween {r} {r}ᶜ

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

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.

theorem SimpleGraph.cliqueFree_starGraph_three {V : Type u_1} (r : V) : (starGraph r).CliqueFree 3

theorem SimpleGraph.eq_starGraph_of_isUniversal_of_cliqueFree_three {V : Type u_1} {G : SimpleGraph V} {v : V} (hv : G.IsUniversal v) (h3 : G.CliqueFree 3) : G = starGraph v

theorem SimpleGraph.IsUniversal.isAcyclic_iff_cliqueFree_three {V : Type u_1} {G : SimpleGraph V} {v : V} (hv : G.IsUniversal v) : G.IsAcyclic ↔ G.CliqueFree 3

theorem SimpleGraph.starGraph_inl_unitMk {V : Type u_1} : starGraph (Sum.inl ()) = completeBipartiteGraph Unit V

theorem SimpleGraph.starGraph_inr_unitMk {V : Type u_1} : starGraph (Sum.inr ()) = completeBipartiteGraph V Unit