toSubgraph_le_induce_support — Mathlib

English

The subgraph obtained from a walk is contained in the subgraph induced by the vertices that appear in the walk’s support.

Русский

Подграф, полученный из обхода, содержится в подграфе, индуцируемом вершинами из поддержки обхода.

LaTeX

$$$ p.toSubgraph \le (\top : G.Subgraph).induce \{v \mid v \in p.support\} $$$

Lean4

theorem toSubgraph_le_induce_support (p : G.Walk u v) : p.toSubgraph ≤ (⊤ : G.Subgraph).induce {v | v ∈ p.support} :=
  by
  convert Subgraph.le_induce_top_verts
  exact p.verts_toSubgraph.symm

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