toSubgraph_adj_getVert — Mathlib

English

For a walk w and any index i with i < length(w), the i-th and (i+1)-th vertices are adjacent in the subgraph.

Русский

Для обхода w и любого i < длины обхода вершины на позициях i и i+1 смежны в подграфе.

LaTeX

$$$ w.toSubgraph.Adj (w.getVert i) (w.getVert (i + 1)) $$$

Lean4

theorem toSubgraph_adj_getVert {u v} (w : G.Walk u v) {i : ℕ} (hi : i < w.length) :
    w.toSubgraph.Adj (w.getVert i) (w.getVert (i + 1)) := by
  induction w generalizing i with
  | nil => cases hi
  | cons hxy i' ih =>
    cases i
    ·
      simp only [Walk.toSubgraph, Walk.getVert_zero, zero_add, getVert_cons_succ, Subgraph.sup_adj, subgraphOfAdj_adj,
        true_or]
    · simp only [Walk.toSubgraph, getVert_cons_succ, Subgraph.sup_adj, subgraphOfAdj_adj, Sym2.eq, Sym2.rel_iff',
        Prod.mk.injEq, Prod.swap_prod_mk]
      right
      exact ih (Nat.succ_lt_succ_iff.mp hi)

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