reachable_toSimpleGraph — Mathlib

English

Let C be a connected component of G. Then for any u,v ∈ V with u ∈ C and v ∈ C, there exists a path in the induced component graph from u to v.

Русский

Пусть C — компонент связности графа G. Тогда для любых u, v ∈ V с u ∈ C и v ∈ C существует путь в порожденном компоненте графа от u до v.

LaTeX

$$$ C.toSimpleGraph.Reachable \\langle u, hu \\rangle \\langle v, hv \\rangle $$$

Lean4

theorem reachable_toSimpleGraph {G : SimpleGraph V} (C : G.ConnectedComponent) {u v : V} (hu : u ∈ C) (hv : v ∈ C) :
    C.toSimpleGraph.Reachable ⟨u, hu⟩ ⟨v, hv⟩ :=
  Walk.reachable (C.walk_toSimpleGraph hu hv)

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