English
An edge between u' and v' exists in the subgraph of walk w if and only if there is an index i with the pair {w_i, w_{i+1}} equal to {u',v'} and i < length(w).
Русский
Смежность между u' и v' в подграфе обхода существует тогда и только тогда, когда существует индекс i, для которого пара вершин обхода совпадает с {u',v'} и i < длины обхода.
LaTeX
$$$ w.toSubgraph.Adj u' v' \iff \exists i, \{w.getVert i, w.getVert (i+1)\} = \{u', v'\} \land i < w.length $$$
Lean4
theorem toSubgraph_adj_iff {u v u' v'} (w : G.Walk u v) :
w.toSubgraph.Adj u' v' ↔ ∃ i, s(w.getVert i, w.getVert (i + 1)) = s(u', v') ∧ i < w.length :=
by
constructor
· intro hadj
unfold Walk.toSubgraph at hadj
match w with
| .nil => simp only [singletonSubgraph_adj, Pi.bot_apply, «Prop».bot_eq_false] at hadj
|
.cons h
p =>
simp only [Subgraph.sup_adj, subgraphOfAdj_adj, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk] at hadj
cases hadj with
| inl hl =>
use 0
simp only [Walk.getVert_zero, zero_add, getVert_cons_succ]
refine ⟨?_, by simp only [length_cons, Nat.zero_lt_succ]⟩
exact Sym2.eq_iff.mpr hl
| inr hr =>
obtain ⟨i, hi⟩ := (toSubgraph_adj_iff _).mp hr
use i + 1
simp only [getVert_cons_succ]
constructor
· exact hi.1
· simp only [Walk.length_cons, Nat.add_lt_add_right hi.2 1]
· rintro ⟨i, hi⟩
rw [← Subgraph.mem_edgeSet, ← hi.1, Subgraph.mem_edgeSet]
exact toSubgraph_adj_getVert _ hi.2
