toSimpleGraph_adj — Mathlib

English

Let C be a connected component of a simple graph G. For any u, v ∈ V with u ∈ C and v ∈ C, the adjacency relation in the component graph equals the adjacency relation in G: C.toSimpleGraph.Adj ⟨u, hu⟩ ⟨v, hv⟩ ↔ G.Adj u v.

Русский

Пусть C — компонент связности графа G. Для любых вершин u, v ∈ V, принадлежащих C, смежность в графе, порождаемом компонентой, равна смежности в G: C.toSimpleGraph.Adj ⟨u, hu⟩ ⟨v, hv⟩ ↔ G.Adj u v.

LaTeX

$$$ C.toSimpleGraph.Adj \\langle u, hu \\rangle \\langle v, hv \\rangle \\leftrightarrow G.Adj u v $$$

Lean4

theorem toSimpleGraph_adj {G : SimpleGraph V} (C : G.ConnectedComponent) {u v : V} (hu : u ∈ C) (hv : v ∈ C) :
    C.toSimpleGraph.Adj ⟨u, hu⟩ ⟨v, hv⟩ ↔ G.Adj u v := by simp [toSimpleGraph]

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