lineGraph_adj_iff_exists — Mathlib

English

In the line graph, adjacency of edges e1 and e2 occurs exactly when e1 ≠ e2 and there exists a vertex v belonging to both edges.

Русский

В линейном графе смежность рёбер e1 и e2 происходит тогда, когда e1 ≠ e2 и существует вершина v, принадлежащая обоим рёбрам.

LaTeX

$$$$ (G.lineGraph).Adj e_1 e_2 \\iff e_1 \\neq e_2 \\wedge \\exists v, v \\in (e_1 : \\mathrm{Sym2} V) \\wedge v \\in (e_2 : \\mathrm{Sym2} V). $$$$

Lean4

theorem lineGraph_adj_iff_exists {e₁ e₂ : G.edgeSet} :
    (G.lineGraph).Adj e₁ e₂ ↔ e₁ ≠ e₂ ∧ ∃ v, v ∈ (e₁ : Sym2 V) ∧ v ∈ (e₂ : Sym2 V) := by simp [Set.Nonempty, lineGraph]

Похожие утверждения