LineGraph

Main definitions

• SimpleGraph.lineGraph is the line graph of a simple graph G, with vertices as the edges of G and two vertices of the line graph adjacent if the corresponding edges share a vertex in G.

Tags

line graph

def SimpleGraph.lineGraph {V : Type u_2} (G : SimpleGraph V) : SimpleGraph ↑G.edgeSet

The line graph of a simple graph G has its vertex set as the edges of G, and two vertices of the line graph are adjacent if the corresponding edges share a vertex in G.

Equations

• G.lineGraph = { Adj := fun (e₁ e₂ : ↑G.edgeSet) => e₁ ≠ e₂ ∧ (↑↑e₁ ∩ ↑↑e₂).Nonempty, symm := ⋯, loopless := ⋯ }

theorem SimpleGraph.lineGraph_adj_iff_exists {V : Type u_1} {G : SimpleGraph V} {e₁ e₂ : ↑G.edgeSet} : G.lineGraph.Adj e₁ e₂ ↔ e₁ ≠ e₂ ∧ ∃ v ∈ ↑e₁, v ∈ ↑e₂

@[simp]

theorem SimpleGraph.lineGraph_bot {V : Type u_1} : ⊥.lineGraph = ⊥