toSubgraph_connected — Mathlib

English

For any walk p in G from u to v, the subgraph induced by p is connected.

Русский

Для любого обхода p в G от u к v подграф, индуцируемый обходом, является связным.

LaTeX

$$$ p.toSubgraph.Connected $$$

Lean4

theorem _root_.SimpleGraph.Walk.toSubgraph_connected {u v : V} (p : G.Walk u v) : p.toSubgraph.Connected := by
  induction p with
  | nil => apply singletonSubgraph_connected
  | @cons _ w _ h p ih =>
    apply (subgraphOfAdj_connected h).sup ih
    exists w
    simp

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