connected_induce_support — Mathlib

English

For any walk p, the subgraph induced by the vertices visited by p is connected.

Русский

Для любой прогулки p граф, индуцированный вершинами, посещёнными во время p, связен.

LaTeX

$$For all p : G.Walk u v, (G.induce {v | v ∈ p.support}).Connected$$

Lean4

theorem connected_induce_support {u v : V} (p : G.Walk u v) : (G.induce {v | v ∈ p.support}).Connected :=
  by
  rw [← p.verts_toSubgraph]
  exact p.toSubgraph_connected.induce_verts

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