English
The line graph L(G) has vertex set equal to the edges of G, and two vertices of L(G) are adjacent if the corresponding edges share a vertex in G.
Русский
Линейный граф L(G) имеет вершины, соответствующие ребрам G, а две вершины L(G) соседни тогда и только тогда, когда соответствующие ребра G имеют общую вершину.
LaTeX
$$$$ \\mathrm{lineGraph}(G) \\text{ has vertex set } G.edgeSet, \\quad \\text{Adj}_{L(G)}(e_1,e_2) \\iff e_1 \\neq e_2 \\wedge (e_1 \\cap e_2) \\neq \\emptyset. $$$$
Lean4
/-- 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`.
-/
def lineGraph {V : Type*} (G : SimpleGraph V) : SimpleGraph G.edgeSet
where
Adj e₁ e₂ := e₁ ≠ e₂ ∧ (e₁ ∩ e₂ : Set V).Nonempty
symm e₁ e₂ := by intro h; rwa [ne_comm, Set.inter_comm]
